1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl
5
6 Infinite sum over a topological monoid
7
8 This sum is known as unconditionally convergent, as it sums to the same value under all possible
9 permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute
10 convergence.
11
12 Note: There are summable sequences which are not unconditionally convergent! The other way holds
13 generally, see `tendsto_sum_nat_of_has_sum`.
14
15 Reference:
16 * Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
17
18 -/
19 import logic.function algebra.big_operators data.set.lattice data.finset
src └────────────┘ └───────────────────┘ └──────────────┘ └─────────┘
20 topology.metric_space.basic topology.algebra.uniform_group topology.algebra.ring
src └─────────────────────────┘ └────────────────────────────┘ └───────────────────┘
21 topology.algebra.ordered topology.instances.real
src └──────────────────────┘ └─────────────────────┘
22
23 noncomputable theory
24 open lattice finset filter function classical
25 open_locale topological_space
26 local attribute [instance] classical.prop_decidable -- TODO: use "open_locale classical"
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
27
28 def option.cases_on' {α β} : option α → β → (α → β) → β
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
29 | none n s := n
id └──┘ ┴
src └──┘
typ └──┘ ┴
30 | (some a) n s := s a
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
31
32 variables {α : Type*} {β : Type*} {γ : Type*}
33
34 section has_sum
35 variables [add_comm_monoid α] [topological_space α]
id └─────────────┘ └───────────────┘
src └─────────────┘ └───────────────┘
typ └─────────────┘ └───────────────┘
doc └───────────────┘
36
37 /-- Infinite sum on a topological monoid
38 The `at_top` filter on `finset α` is the limit of all finite sets towards the entire type. So we sum
39 up bigger and bigger sets. This sum operation is still invariant under reordering, and a absolute
40 sum operator.
41
42 This is based on Mario Carneiro's infinite sum in Metamath.
43
44 For the definition or many statements, α does not need to be a topological monoid. We only add
45 this assumption later, for the lemmas where it is relevant.
46 -/
47 def has_sum (f : β → α) (a : α) : Prop := tendsto (λs:finset β, s.sum f) at_top (𝓝 a)
id ┴ ┴ ┴ └─────┘ └────┘ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
src └─────┘ └────┘ └──┘ └────┘ ┴
typ ┴ ┴ ┴ └─────┘ └────┘ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
doc └─────┘ └────┘ └────┘ ┴
48
49 /-- `summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/
50 def summable (f : β → α) : Prop := ∃a, has_sum f a
id ┴ ┴ ┴┴┴ └─────┘ ┴ ┴
src ┴ ┴ └─────┘
typ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴
doc └─────┘
51
52 /-- `tsum f` is the sum of `f` it exists, or 0 otherwise -/
53 def tsum (f : β → α) := if h : summable f then classical.some h else 0
id ┴ ┴ └┘ └──────┘ ┴ └────────────┘ ┴ ┴
src └┘ └──────┘ └────────────┘ ┴
typ ┴ ┴ └┘ └──────┘ ┴ └────────────┘ ┴ ┴
doc └──────┘
54
55 notation `∑` binders `, ` r:(scoped f, tsum f) := r
id └──┘
src └──┘
typ └──┘
doc └──┘
56
57 variables {f g : β → α} {a b : α} {s : finset β}
id └────┘
src └────┘
typ └────┘
doc └────┘
58
59 lemma has_sum_tsum (ha : summable f) : has_sum f (∑b, f b) :=
id └──────┘ ┴ └─────┘ ┴ ┴┴┴ ┴ ┴
src └──────┘ └─────┘ ┴ ┴
typ └──────┘ ┴ └─────┘ ┴ ┴┴┴ ┴ ┴
doc └──────┘ └─────┘ ┴ ┴
60 by simp [ha, tsum]; exact some_spec ha
id └┘ └──┘ └───────┘ └┘
src └────┘ └┘└──┘┴ └────┘└───────┘┴ └
typ └────┘└┘└┘└──┘┴ └────┘└───────┘┴└┘└
doc └────┘ └┘└──┘┴ └────┘ ┴ └
txt └────┘ └┘ ┴ └────┘ ┴ └
par └────┘ └┘ ┴ └────┘ ┴ └
pid ┴┴ └┘ ┴ ┴ ┴ └
st └────────────────────────────────────
61
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
62 lemma summable_spec (ha : has_sum f a) : summable f := ⟨a, ha⟩
id └─────┘ ┴ ┴ └──────┘ ┴ ┴ └┘
src └─────┘ └──────┘
typ └─────┘ ┴ ┴ └──────┘ ┴ ┴ └┘
doc └─────┘ └──────┘
63
64 /-- Constant zero function has sum `0` -/
65 lemma has_sum_zero : has_sum (λb, 0 : β → α) 0 :=
id └─────┘ ┴ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴ ┴
doc └─────┘
66 by simp [has_sum, tendsto_const_nhds]
id └─────┘ └────────────────┘
src └────┘└─────┘└┘└────────────────┘└─
typ └────┘└─────┘└┘└────────────────┘└─
doc └────┘└─────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────
67
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
68 lemma summable_zero : summable (λb, 0 : β → α) := summable_spec has_sum_zero
id └──────┘ ┴ ┴ ┴ └───────────┘ └──────────┘
src └──────┘ └───────────┘ └──────────┘
typ └──────┘ ┴ ┴ ┴ └───────────┘ └──────────┘
doc └──────┘ └──────────┘
69
70 /-- If a function `f` vanishes outside of a finite set `s`, then it `has_sum` `s.sum f`. -/
71 lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f (s.sum f) :=
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
src ┴ ┴ └─────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
doc └─────┘
72 tendsto_infi' s $ tendsto.congr'
id └───────────┘ ┴ └────────────┘
src └───────────┘ └────────────┘
typ └───────────┘ ┴ └────────────┘
73 (assume t (ht : s ⊆ t), show s.sum f = t.sum f, from sum_subset ht $ assume x _, hf _)
id ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └────────┘ └┘ ┴ ┴ └┘
src ┴ └──┘ ┴ └──┘ └────────┘
typ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴ └────────┘ └┘ ┴ ┴ └┘
74 tendsto_const_nhds
id └────────────────┘
src └────────────────┘
typ └────────────────┘
75
76 lemma has_sum_fintype [fintype β] (f : β → α) : has_sum f (finset.univ.sum f) :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ └─────────┘└──┘ ┴
src └─────┘ └─────┘ └─────────┘└──┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ └─────────┘└──┘ ┴
doc └─────┘ └─────┘ └─────────┘
77 has_sum_sum_of_ne_finset_zero $ λ a h, h.elim (mem_univ _)
id └───────────────────────────┘ ┴ ┴ ┴└───┘ └──────┘
src └───────────────────────────┘ └───┘ └──────┘
typ └───────────────────────────┘ ┴ ┴ ┴└───┘ └──────┘
doc └───────────────────────────┘
78
79 lemma summable_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : summable f :=
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
80 summable_spec $ has_sum_sum_of_ne_finset_zero hf
id └───────────┘ └───────────────────────────┘ └┘
src └───────────┘ └───────────────────────────┘
typ └───────────┘ └───────────────────────────┘ └┘
doc └───────────────────────────┘
81
82 lemma has_sum_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0) :
id ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
83 has_sum f (f b) :=
id └─────┘ ┴ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴ ┴
doc └─────┘
84 suffices has_sum f (({b} : finset β).sum f),
id └─────┘ ┴ ┴┴ └────┘ ┴ └─┘ ┴
src └─────┘ ┴ └────┘ └─┘
typ └─────┘ ┴ ┴┴ └────┘ ┴ └─┘ ┴
doc └─────┘ └────┘
85 by simpa using this,
id └──┘
src └──────────┘
typ └──────────┘└──┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └───────────────┘
86 has_sum_sum_of_ne_finset_zero $ by simpa [hf]
id └───────────────────────────┘ └┘
src └───────────────────────────┘ └─────┘ └─
typ └───────────────────────────┘ └─────┘└┘└─
doc └───────────────────────────┘ └─────┘ └─
txt └─────┘ └─
par └─────┘ └─
pid ┴┴ ┴└
st └───────────
87
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
88 lemma has_sum_ite_eq (b : β) (a : α) : has_sum (λb', if b' = b then a else 0) a :=
id ┴ ┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ ┴ ┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └─────┘
89 begin
st └─────
90 convert has_sum_single b _,
id └────────────┘ ┴
src └──────┘└────────────┘┴ └┘
typ └──────┘└────────────┘┴┴└┘
doc └──────┘ ┴ └┘
txt └──────┘ ┴ └┘
par └──────┘ ┴ └┘
pid ┴ ┴ └┘
st ───────────────────────────┘└─
91 { exact (if_pos rfl).symm },
id └────┘ └─┘
src └────┘ └────┘┴└─┘└─────┘
typ └────┘ └────┘┴└─┘└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ───┘└──────────────────────┘└┘└
92 assume b' hb',
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ──────────────┘└─
93 exact if_neg hb'
id └────┘ └─┘
src └────┘└────┘┴ ┴
typ └────┘└────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────┘
94 end
st └─┘
95
96 lemma has_sum_of_iso {j : γ → β} {i : β → γ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
97 (hf : has_sum f a) (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) : has_sum (f ∘ j) a :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
98 have ∀x y, j x = j y → x = y,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
99 from assume x y h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
100 have i (j x) = i (j y), by rw [h],
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘┴┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └────┘┴
101 by rwa [h₁, h₁] at this,
id └┘ └┘
src └───┘ └┘ └───────┘
typ └───┘└┘└┘└┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st └──────┘└──┘┴└──────┘
102 have (λs:finset γ, s.sum (f ∘ j)) = (λs:finset β, s.sum f) ∘ (λs:finset γ, s.image j),
id └────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└──┘ ┴ ┴ └────┘ ┴ ┴└────┘ ┴
src └────┘ └──┘ ┴ ┴ └────┘ └──┘ ┴ └────┘ └────┘
typ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└──┘ ┴ ┴ └────┘ ┴ ┴└────┘ ┴
doc └────┘ └────┘ └────┘ └────┘
103 from funext $ assume s, (sum_image $ assume x _ y _, this x y).symm,
id └────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘
src └────┘ └───────┘ └──┘
typ └────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘
104 show tendsto (λs:finset γ, s.sum (f ∘ j)) at_top (𝓝 a),
id └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └─────┘ └────┘ └──┘ ┴ └────┘ ┴
typ └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └─────┘ └────┘ └────┘ ┴
105 by rw [this]; apply hf.comp (tendsto_finset_image_at_top_at_top h₂)
id └──┘ └─────┘ └────────────────────────────────┘ └┘
src └──┘ ┴ └────┘└─────┘┴ └────────────────────────────────┘┴ └─
typ └──┘└──┘┴ └────┘└─────┘┴ └────────────────────────────────┘┴└┘└─
doc └──┘ ┴ └────┘ ┴ ┴ └─
txt └──┘ ┴ └────┘ ┴ ┴ └─
par └──┘ ┴ └────┘ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ ┴ ┴└
st └───────┘┴└───────────────────────────────────────────────────────
106
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
107 lemma has_sum_iff_has_sum_of_iso {j : γ → β} (i : β → γ)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
108 (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
109 has_sum (f ∘ j) a ↔ has_sum f a :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
110 iff.intro
id └───────┘
src └───────┘
typ └───────┘
111 (assume hfj,
id └─┘
typ └─┘
112 have has_sum ((f ∘ j) ∘ i) a, from has_sum_of_iso hfj h₂ h₁,
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └┘ └┘
src └─────┘ ┴ ┴ └────────────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └─┘ └┘ └┘
doc └─────┘
113 by simp [(∘), h₂] at this; assumption)
id ┴ └┘
src └────┘┴└──┘ └───────┘ └────────┘
typ └────┘┴└──┘└┘└───────┘ └────────┘
doc └────┘ └──┘ └───────┘ └────────┘
txt └────┘ └──┘ └───────┘ └────────┘
par └────┘ └──┘ └───────┘ └────────┘
pid ┴┴ └──┘ ┴┴└─────┘
st └─────────────────────────────────┘
114 (assume hf, has_sum_of_iso hf h₁ h₂)
id └┘ └────────────┘ └┘ └┘ └┘
src └────────────┘
typ └┘ └────────────┘ └┘ └┘ └┘
115
116 lemma has_sum_hom (g : α → γ) [add_comm_monoid γ] [topological_space γ]
id ┴ ┴ └─────────────┘ ┴ └───────────────┘ ┴
src └─────────────┘ └───────────────┘
typ ┴ ┴ └─────────────┘ ┴ └───────────────┘ ┴
doc └───────────────┘
117 [is_add_monoid_hom g] (h₃ : continuous g) (hf : has_sum f a) :
id └───────────────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴
src └───────────────┘ └────────┘ └─────┘
typ └───────────────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴
doc └───────────────┘ └────────┘ └─────┘
118 has_sum (g ∘ f) (g a) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
119 have (λs:finset β, s.sum (g ∘ f)) = g ∘ (λs:finset β, s.sum f),
id └────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└──┘ ┴
src └────┘ └──┘ ┴ ┴ ┴ └────┘ └──┘
typ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴└──┘ ┴
doc └────┘ └────┘
120 from funext $ assume s, s.sum_hom g,
id └────┘ ┴ ┴└──────┘ ┴
src └────┘ └──────┘
typ └────┘ ┴ ┴└──────┘ ┴
121 show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (𝓝 (g a)),
id └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └─────┘ └────┘ └──┘ ┴ └────┘ ┴
typ └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └─────┘ └────┘ └────┘ ┴
122 by rw [this]; exact tendsto.comp (continuous_iff_continuous_at.mp h₃ a) hf
id └──┘ └──────────┘ └─────────────────────────────┘ └┘ ┴ └┘
src └──┘ ┴ └────┘└──────────┘┴ └─────────────────────────────┘┴ ┴ └┘ └
typ └──┘└──┘┴ └────┘└──────────┘┴ └─────────────────────────────┘┴└┘┴┴└┘└┘└
doc └──┘ ┴ └────┘ ┴ ┴ ┴ └┘ └
txt └──┘ ┴ └────┘ ┴ ┴ ┴ └┘ └
par └──┘ ┴ └────┘ ┴ ┴ ┴ └┘ └
pid └┘ ┴ ┴ ┴ ┴ ┴ └┘ └
st └───────┘┴└──────────────────────────────────────────────────────────────
123
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
124 /-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/
125 lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) :
id ┴ ┴ └─────┘ ┴ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
126 tendsto (λn:ℕ, (range n).sum f) at_top (𝓝 a) :=
id └─────┘ ┴ └───┘ ┴ └─┘ ┴ └────┘ ┴ ┴
src └─────┘ ┴ └───┘ └─┘ └────┘ ┴
typ └─────┘ ┴ └───┘ ┴ └─┘ ┴ └────┘ ┴ ┴
doc └─────┘ └───┘ └────┘ ┴
127 @tendsto.comp _ _ _ finset.range (λ s : finset ℕ, s.sum f) _ _ _ h tendsto_finset_range
id └──────────┘ └──────────┘ └────┘ ┴ ┴└──┘ ┴ ┴ └──────────────────┘
src └──────────┘ └──────────┘ └────┘ ┴ └──┘ └──────────────────┘
typ └──────────┘ └──────────┘ └────┘ ┴ ┴└──┘ ┴ ┴ └──────────────────┘
doc └──────────┘ └────┘
128
129 variable [topological_add_monoid α]
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
130
131 lemma has_sum_add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) :=
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
132 by simp [has_sum, sum_add_distrib]; exact hf.add hg
id └─────┘ └─────────────┘ └────┘ └┘
src └────┘└─────┘└┘└─────────────┘┴ └────┘└────┘┴ └
typ └────┘└─────┘└┘└─────────────┘┴ └────┘└────┘┴└┘└
doc └────┘└─────┘└┘ ┴ └────┘ ┴ └
txt └────┘ └┘ ┴ └────┘ ┴ └
par └────┘ └┘ ┴ └────┘ ┴ └
pid ┴┴ └┘ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────
133
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
134 lemma summable_add (hf : summable f) (hg : summable g) : summable (λb, f b + g b) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
135 summable_spec $ has_sum_add (has_sum_tsum hf)(has_sum_tsum hg)
id └───────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
src └───────────┘ └─────────┘ └──────────┘ └──────────┘
typ └───────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
136
137 lemma has_sum_sum {f : γ → β → α} {a : γ → α} {s : finset γ} :
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
doc └────┘
138 (∀i∈s, has_sum (f i) (a i)) → has_sum (λb, s.sum $ λi, f i b) (s.sum a) :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴
src └─────┘ └─────┘ └──┘ └──┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴
doc └─────┘ └─────┘
139 finset.induction_on s (by simp [has_sum_zero]) (by simp [has_sum_add] {contextual := tt})
id └─────────────────┘ ┴ └──────────┘ └─────────┘ └┘
src └─────────────────┘ └────┘└──────────┘┴ └────┘└─────────┘└┘ └────────────┘└┘┴
typ └─────────────────┘ ┴ └────┘└──────────┘┴ └────┘└─────────┘└┘ └────────────┘└┘┴
doc └─────────────────┘ └────┘└──────────┘┴ └────┘ └┘ └────────────┘ ┴
txt └────┘ ┴ └────┘ └┘ └────────────┘ ┴
par └────┘ ┴ └────┘ └┘ └────────────┘ ┴
pid ┴┴ ┴ ┴┴ ┴┴ └────────────┘ ┴
st └──────────────────┘ └────────────────────────────────────┘
140
141 lemma summable_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └────┘ └──────┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └────┘ └──────┘
142 summable (λb, s.sum $ λi, f i b) :=
id └──────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └──────┘ └──┘
typ └──────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────┘
143 summable_spec $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
id └───────────┘ └─────────┘ ┴ └┘ └──────────┘ └┘ ┴ └┘
src └───────────┘ └─────────┘ └──────────┘
typ └───────────┘ └─────────┘ ┴ └┘ └──────────┘ └┘ ┴ └┘
144
145 lemma has_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
id └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
146 (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) (ha : has_sum f a) : has_sum g a :=
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘ └─────┘
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘ └─────┘
147 assume s' hs',
148 let
149 ⟨s, hs, hss', hsc⟩ := nhds_is_closed hs',
id └────────────┘
src └────────────┘
typ └────────────┘
150 ⟨u, hu⟩ := mem_at_top_sets.mp $ ha hs,
151 fsts := u.image sigma.fst,
id └───────┘
src └───────┘
typ └───────┘
152 snds := λb, u.bind (λp, (if h : p.1 = b then {cast (congr_arg γ h) p.2} else ∅ : finset (γ b)))
id └───────┘ └────┘
src └───────┘ └────┘
typ └───────┘ └────┘
doc └────┘
153 in
154 have u_subset : u ⊆ fsts.sigma snds,
155 from subset_iff.mpr $ assume ⟨b, c⟩ hu,
156 have hb : b ∈ fsts, from finset.mem_image.mpr ⟨_, hu, rfl⟩,
id └─┘
src └─┘
typ └─┘
157 have hc : c ∈ snds b, from mem_bind.mpr ⟨_, hu, by simp; refl⟩,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
158 by simp [mem_sigma, hb, hc] ,
src └────┘ └┘ └┘ └┘
typ └────┘ └┘ └┘ └┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
159 mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
id └──────────┘
src └──────────┘
typ └──────────┘
160 have h : ∀cs : Π b ∈ bs, finset (γ b),
id └────┘
src └────┘
typ └────┘
doc └────┘
161 ((⋂b (hb : b ∈ bs), (λp:Πb, finset (γ b), p b) ⁻¹' {cs' | cs b hb ⊆ cs' }) ∩
id └────┘
src └────┘
typ └────┘
doc └────┘
162 (λp, bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩))) ⁻¹' s).nonempty,
163 from assume cs,
164 let cs' := λb, (if h : b ∈ bs then cs b h else ∅) ∪ snds b in
165 have sum_eq : bs.sum (λb, (cs' b).sum (λc, f ⟨b, c⟩)) = (bs.sigma cs').sum f,
166 from sum_sigma.symm,
167 have (bs.sigma cs').sum f ∈ s,
168 from hu _ $ finset.subset.trans u_subset $ sigma_mono hbs $
id └─────────────────┘ └────────┘
src └─────────────────┘ └────────┘
typ └─────────────────┘ └────────┘
169 assume b, @finset.subset_union_right (γ b) _ _ _,
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
170 exists.intro cs' $
id └──────────┘
src └──────────┘
typ └──────────┘
171 by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_right] },
src └────┘ └┘ ┴ └─────────┘ └────┘ └┘ └┘ └┘
typ └────┘ └┘ ┴ └─────────┘ └────┘ └┘ └┘ └┘
doc └────┘ └┘ ┴ └─────────┘ └────┘ └┘ └┘ └┘
txt └────┘ └┘ ┴ └─────────┘ └────┘ └┘ └┘ └┘
par └────┘ └┘ ┴ └─────────┘ └────┘ └┘ └┘ └┘
pid ┴┴ └┘ ┴ └───┘ ┴┴ └┘ └┘ ┴┴
172 have tendsto (λp:(Πb:β, finset (γ b)), bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩)))
id └────┘
src └────┘
typ └────┘
doc └────┘
173 (⨅b (h : b ∈ bs), at_top.comap (λp, p b)) (𝓝 (bs.sum g)),
174 from tendsto_finset_sum bs $
id └────────────────┘
src └────────────────┘
typ └────────────────┘
175 assume c hc, tendsto_infi' c $ tendsto_infi' hc $ by apply tendsto.comp (hf c) tendsto_comap,
id └───────────┘ └───────────┘
src └───────────┘ └───────────┘ └────┘ ┴ ┴ └┘
typ └───────────┘ └───────────┘ └────┘ ┴ ┴ └┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
176 have bs.sum g ∈ s,
177 from mem_of_closed_of_tendsto' this hsc $ forall_sets_nonempty_iff_ne_bot.mp $
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
178 by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib,
id └───────┘ └─────┘ └────────────────┘
src └────┘ └┘ └───────┘└┘└─────┘└┘└────────────────┘└─
typ └────┘ └┘ └───────┘└┘└─────┘└┘└────────────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └─
st └───────────────────────────────────────
179 filter.mem_infi_sets_finset, mem_comap_sets, skolem, mem_at_top_sets,
id └─────────────────────────┘ └────────────┘ └────┘ └─────────────┘
src ──────────────┘└─────────────────────────┘└┘└────────────┘└┘└────┘└┘└─────────────┘└─
typ ──────────────┘└─────────────────────────┘└┘└────────────┘└┘└────┘└┘└─────────────┘└─
doc ──────────────┘ └┘ └┘ └┘ └─
txt ──────────────┘ └┘ └┘ └┘ └─
par ──────────────┘ └┘ └┘ └┘ └─
pid ──────────────┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────
180 and_comm];
id └──────┘
src ──────────────┘└──────┘┴
typ ──────────────┘└──────┘┴
doc ──────────────┘ ┴
txt ──────────────┘ ┴
par ──────────────┘ ┴
pid ──────────────┘ ┴
st ──────────────────────────
181 from
src └────
typ └────
doc └────
txt └────
par └────
pid └────
st ───────────
182 assume s₁ s₂ s₃ hs₁ hs₃ p hs₂ p' hp cs hp',
src ───────┘ └─────────────────────────────────────
typ ───────┘ └─────────────────────────────────────
doc ───────┘ └─────────────────────────────────────
txt ───────┘ └─────────────────────────────────────
par ───────┘ └─────────────────────────────────────
pid ───────┘ └─────────────────────────────────────
st ────────────────────────────────────────────────────
183 have (⋂b (h : b ∈ bs), (λp:(Πb, finset (γ b)), p b) ⁻¹' {cs' | cs b h ⊆ cs' }) ≤ (⨅b∈bs, p b),
id ┴ ┴ ┴ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘┴
src ───────┘ ┴ ┴└─────┘ ┴┴┴ ┴┴┴ └┘ ┴ ┴└────┘┴ ┴ └──┘ ┴ └┘└─┘┴┴└────┘ ┴ ┴ ┴┴┴ └──┘┴┴ ┴└┘ ┴┴ ┴ └──
typ ───────┘ ┴ ┴└─────┘ ┴┴┴ ┴┴┴ └┘ ┴ ┴└────┘┴ ┴┴ └──┘ ┴ └┘└─┘┴┴└────┘ ┴ ┴ ┴┴┴ └──┘┴┴ ┴└┘└┘┴┴ ┴ └──
doc ───────┘ ┴ ┴└─────┘ ┴ ┴ ┴┴┴ └┘ ┴ ┴└────┘┴ ┴ └──┘ ┴ └┘└─┘┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└┘ ┴┴ ┴ └──
txt ───────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └──
par ───────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └──
pid ───────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────────────────────────────────────────
184 from infi_le_infi $ assume b, infi_le_infi $ assume hb,
id └──────────┘
src ──────────────┘ ┴ ┴ └──┘└──────────┘┴ ┴ └────
typ ──────────────┘ ┴ ┴ └──┘└──────────┘┴ ┴ └────
doc ──────────────┘ ┴ ┴ └──┘ ┴ ┴ └────
txt ──────────────┘ ┴ ┴ └──┘ ┴ ┴ └────
par ──────────────┘ ┴ ┴ └──┘ ┴ ┴ └────
pid ──────────────┘ ┴ ┴ └──┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────
185 le_trans (set.preimage_mono $ hp' b hb) (hp b hb),
id └──────┘ └───────────────┘
src ───────────┘└──────┘┴ └───────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
typ ───────────┘└──────┘┴ └───────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
doc ───────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
txt ───────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
par ───────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
pid ───────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────
186 (h _).mono (set.subset.trans (set.inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
id ┴ └──────────────┘ └────────────────────┘
src ───────┘ └───────┘ └──────────────┘┴ └────────────────────┘┴ ┴ ┴ └┘ └┘ ┴
typ ───────┘ ┴└───────┘ └──────────────┘┴ └────────────────────┘┴ ┴ ┴ └┘ └┘ ┴
doc ───────┘ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
txt ───────┘ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
par ───────┘ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
pid ───────┘ └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘
187 hss' this
id └──┘
typ └──┘
188
189 lemma summable_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
id └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └───────────┘
190 (hf : ∀b, summable (λc, f ⟨b, c⟩)) (ha : summable f) : summable (λb, ∑c, f ⟨b, c⟩) :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘ ┴ ┴
191 summable_spec $ has_sum_sigma (assume b, has_sum_tsum $ hf b) (has_sum_tsum ha)
id └───────────┘ └───────────┘ ┴ └──────────┘ └┘ ┴ └──────────┘ └┘
src └───────────┘ └───────────┘ └──────────┘ └──────────┘
typ └───────────┘ └───────────┘ ┴ └──────────┘ └┘ ┴ └──────────┘ └┘
192
193 end has_sum
194
195 section has_sum_iff_has_sum_of_iso_ne_zero
196 variables [add_comm_monoid α] [topological_space α]
id └─────────────┘ └───────────────┘
src └─────────────┘ └───────────────┘
typ └─────────────┘ └───────────────┘
doc └───────────────┘
197 variables {f : β → α} {g : γ → α} {a : α}
198
199 lemma has_sum_of_has_sum
200 (h_eq : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
id └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
typ └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
doc └────┘ └────┘
201 (hf : has_sum g a) : has_sum f a :=
id └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
202 suffices at_top.map (λs:finset β, s.sum f) ≤ at_top.map (λs:finset γ, s.sum g),
id └────┘└──┘ └────┘ ┴ ┴└──┘ ┴ ┴ └────┘└──┘ └────┘ ┴ ┴└──┘ ┴
src └────┘└──┘ └────┘ └──┘ ┴ └────┘└──┘ └────┘ └──┘
typ └────┘└──┘ └────┘ ┴ ┴└──┘ ┴ ┴ └────┘└──┘ └────┘ ┴ ┴└──┘ ┴
doc └────┘└──┘ └────┘ └────┘└──┘ └────┘
203 from le_trans this hf,
id └──────┘ └──┘ └┘
src └──────┘
typ └──────┘ └──┘ └┘
204 by rw [map_at_top_eq, map_at_top_eq];
id └───────────┘ └───────────┘
src └──┘└───────────┘└┘└───────────┘┴
typ └──┘└───────────┘└┘└───────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────────┘└─────────────┘┴└─
205 from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
id └─────┘ ┴ └──┘ └───────────┘
src └───┘ └─────┘┴ ┴ └──┘ ┴ └┘ └───┘ ┴ └──┘└───────────┘┴ ┴ └
typ └───┘ └─────┘┴ ┴ └──┘ ┴ ┴└┘ └───┘└──┘┴ └──┘└───────────┘┴ ┴ └
doc └───┘ ┴ ┴ └──┘ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └
txt └───┘ ┴ ┴ └──┘ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └
par └───┘ ┴ ┴ └──┘ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └
pid └───┘ ┴ ┴ └──┘ ┴ └┘ └───┘ ┴ └──┘ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────
206 by simp [set.image_subset_iff]; exact hv)
id └──────────────────┘ └┘
src ─┘ ┴└────┘└──────────────────┘┴└┘└────┘ └─
typ ─┘ ┴└────┘└──────────────────┘┴└──────┘└┘└─
doc ─┘ ┴└────┘└──────────────────┘┴└┘└────┘ └─
txt ─┘ ┴└────┘ ┴└┘└────┘ └─
par ─┘ ┴└────┘ ┴└──────┘ └─
pid ─┘ └─────┘ └───────┘ ┴└
st ───┘└────────────────────────────────────┘└─
207
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
208 lemma has_sum_iff_has_sum
209 (h₁ : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
id └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
typ └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
doc └────┘ └────┘
210 (h₂ : ∀v:finset β, ∃u:finset γ, ∀u', u ⊆ u' → ∃v', v ⊆ v' ∧ v'.sum f = u'.sum g) :
id └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
typ └────┘ ┴ ┴ └────┘ ┴┴ └┘ ┴ ┴ └┘ ┴└┘┴ ┴ ┴ └┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
doc └────┘ └────┘
211 has_sum f a ↔ has_sum g a :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
212 ⟨has_sum_of_has_sum h₂, has_sum_of_has_sum h₁⟩
id └────────────────┘ └┘ └────────────────┘ └┘
src └────────────────┘ └────────────────┘
typ └────────────────┘ └┘ └────────────────┘ └┘
213
214 variables
215 (i : Π⦃c⦄, g c ≠ 0 → β) (hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
216 (j : Π⦃b⦄, f b ≠ 0 → γ) (hj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
217 (hji : ∀⦃c⦄ (h : g c ≠ 0), j (hi h) = c)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
218 (hij : ∀⦃b⦄ (h : f b ≠ 0), i (hj h) = b)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
219 (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
220 include hi hj hji hij hgj
221
222 lemma has_sum_of_has_sum_ne_zero : has_sum g a → has_sum f a :=
id └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
223 have j_inj : ∀x y (hx : f x ≠ 0) (hy : f y ≠ 0), (j hx = j hy ↔ x = y),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
224 from assume x y hx hy,
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
225 ⟨assume h,
id ┴
typ ┴
226 have i (hj hx) = i (hj hy), by simp [h],
id ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴
src ┴ └────┘ ┴
typ ┴ └┘ └┘ ┴ ┴ └┘ └┘ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
227 by rwa [hij, hij] at this; assumption,
id └─┘ └─┘
src └───┘ └┘ └───────┘ └────────┘
typ └───┘└─┘└┘└─┘└───────┘ └────────┘
doc └───┘ └┘ └───────┘ └────────┘
txt └───┘ └┘ └───────┘ └────────┘
par └───┘ └┘ └───────┘ └────────┘
pid └┘ └┘ ┴└──────┘
st └───────┘└───┘┴└──────────────────┘
228 by simp {contextual := tt}⟩,
id └┘
src └───┘ └────────────┘└┘┴
typ └───┘ └────────────┘└┘┴
doc └───┘ └────────────┘ ┴
txt └───┘ └────────────┘ ┴
par └───┘ └────────────┘ ┴
pid ┴ └────────────┘ ┴
st └──────────────────────┘
229 let ii : finset γ → finset β := λu, u.bind $ λc, if h : g c = 0 then ∅ else {i h} in
id └────┘ ┴ ┴ └────┘ ┴ ┴ ┴└───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴
src └────┘ └────┘ └───┘ └┘ ┴ ┴ ┴
typ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴└───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴
doc └────┘ └────┘ └───┘
230 let jj : finset β → finset γ := λv, v.bind $ λb, if h : f b = 0 then ∅ else {j h} in
id └────┘ ┴ ┴ └────┘ ┴ ┴ ┴└───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴
src └────┘ └────┘ └───┘ └┘ ┴ ┴ ┴
typ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴└───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴
doc └────┘ └────┘ └───┘
231 has_sum_of_has_sum $ assume u, exists.intro (ii u) $
id └────────────────┘ ┴ └──────────┘ └┘ ┴
src └────────────────┘ └──────────┘
typ └────────────────┘ ┴ └──────────┘ └┘ ┴
232 assume v hv, exists.intro (u ∪ jj v) $ and.intro (subset_union_left _ _) $
id ┴ └┘ └──────────┘ ┴ ┴ └┘ ┴ └───────┘ └───────────────┘
src └──────────┘ ┴ └───────┘ └───────────────┘
typ ┴ └┘ └──────────┘ ┴ ┴ └┘ ┴ └───────┘ └───────────────┘
233 have ∀c:γ, c ∈ u ∪ jj v → c ∉ jj v → g c = 0,
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
234 from assume c hc hnc, classical.by_contradiction $ assume h : g c ≠ 0,
id ┴ └┘ └─┘ └────────────────────────┘ ┴ ┴ ┴
src └────────────────────────┘ ┴
typ ┴ └┘ └─┘ └────────────────────────┘ ┴ ┴ ┴
235 have c ∈ u,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
236 from (finset.mem_union.1 hc).resolve_right hnc,
id └──────────────┘┴ └┘ └───────────┘ └─┘
src └──────────────┘┴ └───────────┘
typ └──────────────┘┴ └┘ └───────────┘ └─┘
237 have i h ∈ v,
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
238 from hv $ by simp [mem_bind]; existsi c; simp [h, this],
id └┘ └──────┘ ┴ ┴ └──┘
src └────┘└──────┘┴ └──────┘ └────┘ └┘ ┴
typ └┘ └────┘└──────┘┴ └──────┘┴ └────┘┴└┘└──┘┴
doc └────┘ ┴ └──────┘ └────┘ └┘ ┴
txt └────┘ ┴ └──────┘ └────┘ └┘ ┴
par └────┘ ┴ └──────┘ └────┘ └┘ ┴
pid ┴┴ ┴ ┴ ┴┴ └┘ ┴
st └─────────────────────────────────────────┘
239 have j (hi h) ∈ jj v,
id ┴ └┘ ┴ ┴ └┘ ┴
src ┴
typ ┴ └┘ ┴ ┴ └┘ ┴
240 by simp [mem_bind]; existsi i h; simp [h, hi, this],
id └──────┘ ┴ ┴ ┴ └┘ └──┘
src └────┘└──────┘┴ └──────┘ ┴ └────┘ └┘ └┘ ┴
typ └────┘└──────┘┴ └──────┘┴┴┴ └────┘┴└┘└┘└┘└──┘┴
doc └────┘ ┴ └──────┘ ┴ └────┘ └┘ └┘ ┴
txt └────┘ ┴ └──────┘ ┴ └────┘ └┘ └┘ ┴
par └────┘ ┴ └──────┘ ┴ └────┘ └┘ └┘ ┴
pid ┴┴ ┴ ┴ ┴ ┴┴ └┘ └┘ ┴
st └───────────────────────────────────────────────┘
241 by rw [hji h] at this; exact hnc this,
id └─┘ ┴ └─┘ └──┘
src └──┘ ┴ └───────┘ └────┘ ┴
typ └──┘└─┘┴┴└───────┘ └────┘└─┘┴└──┘
doc └──┘ ┴ └───────┘ └────┘ ┴
txt └──┘ ┴ └───────┘ └────┘ ┴
par └──┘ ┴ └───────┘ └────┘ ┴
pid └┘ ┴ ┴└──────┘ ┴ ┴
st └────────┘┴└──────────────────────┘
242 calc (u ∪ jj v).sum g = (jj v).sum g : (sum_subset (subset_union_right _ _) this).symm
id ┴ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────┘ └────────────────┘ └──┘ └──┘
src ┴ └─┘ └─┘ └────────┘ └────────────────┘ └──┘
typ ┴ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────┘ └────────────────┘ └──┘ └──┘
243 ... = v.sum _ : sum_bind $ by intros x _ y _ _; by_cases f x = 0; by_cases f y = 0; simp [*]; cc
id ┴└──┘ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └──────┘ └──────────────┘ └───────┘ ┴ ┴┴└┘ └───────┘ ┴ ┴ └┘ └──────┘ └──
typ ┴└──┘ └──────┘ └──────────────┘ └───────┘┴┴┴┴┴└┘ └───────┘┴┴┴┴ └┘ └──────┘ └──
doc └──────────────┘ └───────┘ ┴ ┴ └┘ └───────┘ ┴ ┴ └┘ └──────┘ └──
txt └──────────────┘ └───────┘ ┴ ┴ └┘ └───────┘ ┴ ┴ └┘ └──────┘ └──
par └──────────────┘ └───────┘ ┴ ┴ └┘ └───────┘ ┴ ┴ └┘ └──────┘ └──
pid └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴└─┘ └
st └───────────────────────────────────────────────────────────────────
244 ... = v.sum f : sum_congr rfl $ by intros x hx; by_cases f x = 0; simp [*]
id ┴└──┘ ┴ └───────┘ └─┘ ┴ ┴
src ───┘ └──┘ └───────┘ └─┘ └─────────┘ └───────┘ ┴ ┴ └┘ └────────
typ ───┘ ┴└──┘ ┴ └───────┘ └─┘ └─────────┘ └───────┘┴┴┴┴ └┘ └────────
doc ───┘ └─────────┘ └───────┘ ┴ ┴ └┘ └────────
txt ───┘ └─────────┘ └───────┘ ┴ ┴ └┘ └────────
par ───┘ └─────────┘ └───────┘ ┴ ┴ └┘ └────────
pid ───┘ └───┘ ┴ ┴ ┴ ┴┴ ┴└─┘└
st ───┘ └────────────────────────────────────────
245
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
246 lemma has_sum_iff_has_sum_of_ne_zero : has_sum f a ↔ has_sum g a :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
247 iff.intro
id └───────┘
src └───────┘
typ └───────┘
248 (has_sum_of_has_sum_ne_zero j hj i hi hij hji $ assume b hb, by rw [←hgj (hi _), hji])
id └────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ ┴ └┘ └─┘ └┘ └─┘
src └────────────────────────┘ └───┘ ┴ └───┘ ┴
typ └────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ ┴ └┘ └───┘└─┘┴ └┘└───┘└─┘┴
doc └───┘ ┴ └───┘ ┴
txt └───┘ ┴ └───┘ ┴
par └───┘ ┴ └───┘ ┴
pid └─┘ ┴ └───┘ ┴
st └──────────────┘└───┘┴
249 (has_sum_of_has_sum_ne_zero i hi j hj hji hij hgj)
id └────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ └─┘
src └────────────────────────┘
typ └────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ └─┘
250
251 lemma summable_iff_summable_ne_zero : summable g ↔ summable f :=
id └──────┘ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
252 exists_congr $
id └──────────┘
src └──────────┘
typ └──────────┘
253 assume a, has_sum_iff_has_sum_of_ne_zero j hj i hi hij hji $
id ┴ └────────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘
src └────────────────────────────┘
typ ┴ └────────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘
254 assume b hb, by rw [←hgj (hi _), hji]
id ┴ └┘ └─┘ └┘ └─┘
src └───┘ ┴ └───┘ └─
typ ┴ └┘ └───┘└─┘┴ └┘└───┘└─┘└─
doc └───┘ ┴ └───┘ └─
txt └───┘ ┴ └───┘ └─
par └───┘ ┴ └───┘ └─
pid └─┘ ┴ └───┘ ┴└
st └──────────────┘└───┘┴└
255
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
256 end has_sum_iff_has_sum_of_iso_ne_zero
257
258 section has_sum_iff_has_sum_of_bij_ne_zero
259 variables [add_comm_monoid α] [topological_space α]
id └─────────────┘ └───────────────┘
src └─────────────┘ └───────────────┘
typ └─────────────┘ └───────────────┘
doc └───────────────┘
260 variables {f : β → α} {g : γ → α} {a : α}
261 (i : Π⦃c⦄, g c ≠ 0 → β)
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
262 (h₁ : ∀⦃c₁ c₂⦄ (h₁ : g c₁ ≠ 0) (h₂ : g c₂ ≠ 0), i h₁ = i h₂ → c₁ = c₂)
id └┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ └┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
263 (h₂ : ∀⦃b⦄, f b ≠ 0 → ∃c (h : g c ≠ 0), i h = b)
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
264 (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
265 include i h₁ h₂ h₃
266
267 lemma has_sum_iff_has_sum_of_ne_zero_bij : has_sum f a ↔ has_sum g a :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
268 have hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
269 from assume c h, by simp [h₃, h],
id ┴ ┴ └┘ ┴
src └────┘ └┘ ┴
typ ┴ ┴ └────┘└┘└┘┴┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └───────────┘
270 let j : Π⦃b⦄, f b ≠ 0 → γ := λb h, some $ h₂ h in
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
src ┴ └──┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
271 have hj : ∀⦃b⦄ (h : f b ≠ 0), ∃(h : g (j h) ≠ 0), i h = b,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
272 from assume b h, some_spec $ h₂ h,
id ┴ ┴ └───────┘ └┘ ┴
src └───────┘
typ ┴ ┴ └───────┘ └┘ ┴
273 have hj₁ : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
274 from assume b h, let ⟨h₁, _⟩ := hj h in h₁,
id ┴ ┴ └─┘ └┘ └┘ ┴
typ ┴ ┴ └─┘ └┘ └┘ ┴
275 have hj₂ : ∀⦃b⦄ (h : f b ≠ 0), i (hj₁ h) = b,
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
276 from assume b h, let ⟨h₁, h₂⟩ := hj h in h₂,
id ┴ ┴ └─┘ └┘ └┘ ┴
typ ┴ ┴ └─┘ └┘ └┘ ┴
277 has_sum_iff_has_sum_of_ne_zero i hi j hj₁
id └────────────────────────────┘ ┴ └┘ ┴ └─┘
src └────────────────────────────┘
typ └────────────────────────────┘ ┴ └┘ ┴ └─┘
278 (assume c h, h₁ (hj₁ _) h $ hj₂ _) hj₂ (assume b h, by rw [←h₃ (hj₁ _), hj₂])
id ┴ ┴ └┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ └┘ └─┘ └─┘
src └───┘ ┴ └───┘ ┴
typ ┴ ┴ └┘ └─┘ ┴ └─┘ └─┘ ┴ ┴ └───┘└┘┴ └─┘└───┘└─┘┴
doc └───┘ ┴ └───┘ ┴
txt └───┘ ┴ └───┘ ┴
par └───┘ ┴ └───┘ ┴
pid └─┘ ┴ └───┘ ┴
st └──────────────┘└───┘┴
279
280 lemma summable_iff_summable_ne_zero_bij : summable f ↔ summable g :=
id └──────┘ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
281 exists_congr $
id └──────────┘
src └──────────┘
typ └──────────┘
282 assume a, has_sum_iff_has_sum_of_ne_zero_bij @i h₁ h₂ h₃
id ┴ └────────────────────────────────┘ ┴ └┘ └┘ └┘
src └────────────────────────────────┘
typ ┴ └────────────────────────────────┘ ┴ └┘ └┘ └┘
283
284 end has_sum_iff_has_sum_of_bij_ne_zero
285
286 section tsum
287 variables [add_comm_monoid α] [topological_space α] [t2_space α]
id └─────────────┘ └───────────────┘ └──────┘
src └─────────────┘ └───────────────┘ └──────┘
typ └─────────────┘ └───────────────┘ └──────┘
doc └───────────────┘ └──────┘
288 variables {f g : β → α} {a a₁ a₂ : α}
289
290 lemma has_sum_unique : has_sum f a₁ → has_sum f a₂ → a₁ = a₂ := tendsto_nhds_unique at_top_ne_bot
id └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘ └─────────────────┘ └───────────┘
src └─────┘ └─────┘ ┴ └─────────────────┘ └───────────┘
typ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘ └─────────────────┘ └───────────┘
doc └─────┘ └─────┘
291
292 lemma tsum_eq_has_sum (ha : has_sum f a) : (∑b, f b) = a := has_sum_unique (has_sum_tsum ⟨a, ha⟩) ha
id └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └────────────┘ └──────────┘ ┴ └┘ └┘
src └─────┘ ┴ ┴ ┴ └────────────┘ └──────────┘
typ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └────────────┘ └──────────┘ ┴ └┘ └┘
doc └─────┘ ┴ ┴
293
294 lemma has_sum_iff_of_summable (h : summable f) : has_sum f a ↔ (∑b, f b) = a :=
id └──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src └──────┘ └─────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──────┘ └─────┘ ┴ ┴
295 iff.intro tsum_eq_has_sum (assume eq, eq ▸ has_sum_tsum h)
id └───────┘ └─────────────┘ └┘ └┘ ┴ └──────────┘ ┴
src └───────┘ └─────────────┘ └┘ └┘ ┴ └──────────┘
typ └───────┘ └─────────────┘ └┘ └┘ ┴ └──────────┘ ┴
296
297 @[simp] lemma tsum_zero : (∑b:β, 0:α) = 0 := tsum_eq_has_sum has_sum_zero
id ┴ ┴┴ ┴ ┴ └─────────────┘ └──────────┘
src ┴ ┴ ┴ └─────────────┘ └──────────┘
typ ┴ ┴┴ ┴ ┴ └─────────────┘ └──────────┘
doc └──┘ ┴ ┴ └──────────┘
298
299 lemma tsum_eq_sum {f : β → α} {s : finset β} (hf : ∀b∉s, f b = 0) :
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
300 (∑b, f b) = s.sum f :=
id ┴┴┴ ┴ ┴ ┴ ┴└──┘ ┴
src ┴ ┴ ┴ └──┘
typ ┴┴┴ ┴ ┴ ┴ ┴└──┘ ┴
doc ┴ ┴
301 tsum_eq_has_sum $ has_sum_sum_of_ne_finset_zero hf
id └─────────────┘ └───────────────────────────┘ └┘
src └─────────────┘ └───────────────────────────┘
typ └─────────────┘ └───────────────────────────┘ └┘
doc └───────────────────────────┘
302
303 lemma tsum_fintype [fintype β] (f : β → α) : (∑b, f b) = finset.univ.sum f :=
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └─────────┘└──┘ ┴
src └─────┘ ┴ ┴ ┴ └─────────┘└──┘
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └─────────┘└──┘ ┴
doc └─────┘ ┴ ┴ └─────────┘
304 tsum_eq_has_sum $ has_sum_fintype f
id └─────────────┘ └─────────────┘ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ └─────────────┘ ┴
305
306 lemma tsum_eq_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0) :
id ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
307 (∑b, f b) = f b :=
id ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
308 tsum_eq_has_sum $ has_sum_single b hf
id └─────────────┘ └────────────┘ ┴ └┘
src └─────────────┘ └────────────┘
typ └─────────────┘ └────────────┘ ┴ └┘
309
310 @[simp] lemma tsum_ite_eq (b : β) (a : α) : (∑b', if b' = b then a else 0) = a :=
id ┴ ┴ ┴└┘┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴└┘┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
311 tsum_eq_has_sum (has_sum_ite_eq b a)
id └─────────────┘ └────────────┘ ┴ ┴
src └─────────────┘ └────────────┘
typ └─────────────┘ └────────────┘ ┴ ┴
312
313 lemma tsum_eq_tsum_of_has_sum_iff_has_sum {f : β → α} {g : γ → α}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
314 (h : ∀{a}, has_sum f a ↔ has_sum g a) : (∑b, f b) = (∑c, g c) :=
id ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴ ┴ ┴
315 by_cases
id └──────┘
src └──────┘
typ └──────┘
316 (assume : ∃a, has_sum f a,
id ┴┴┴ └─────┘ ┴ ┴
src ┴ ┴ └─────┘
typ ┴┴┴ └─────┘ ┴ ┴
doc └─────┘
317 let ⟨a, hfa⟩ := this in
id └─┘ ┴ └─┘ └──┘
typ └─┘ ┴ └─┘ └──┘
318 have hga : has_sum g a, from h.mp hfa,
id └─────┘ ┴ ┴└─┘
src └─────┘ └─┘
typ └─────┘ ┴ ┴└─┘
doc └─────┘
319 by rw [tsum_eq_has_sum hfa, tsum_eq_has_sum hga])
id └─────────────┘ └─┘ └─────────────┘ └─┘
src └──┘└─────────────┘┴ └┘└─────────────┘┴ ┴
typ └──┘└─────────────┘┴└─┘└┘└─────────────┘┴└─┘┴
doc └──┘ ┴ └┘ ┴ ┴
txt └──┘ ┴ └┘ ┴ ┴
par └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ └┘ ┴ ┴
st └──────────────────────┘└───────────────────┘┴
320 (assume hf : ¬ summable f,
id ┴ └──────┘ ┴
src ┴ └──────┘
typ ┴ └──────┘ ┴
doc └──────┘
321 have hg : ¬ summable g, from assume ⟨a, hga⟩, hf ⟨a, h.mpr hga⟩,
id ┴ └──────┘ ┴ ┴┴ └─┘ └┘ ┴└──┘
src ┴ └──────┘ └──┘
typ ┴ └──────┘ ┴ ┴┴ └─┘ └┘ ┴└──┘
doc └──────┘
322 by simp [tsum, hf, hg])
id └──┘ └┘ └┘
src └────┘└──┘└┘ └┘ ┴
typ └────┘└──┘└┘└┘└┘└┘┴
doc └────┘└──┘└┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └──────────────────┘
323
324 lemma tsum_eq_tsum_of_ne_zero {f : β → α} {g : γ → α}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
325 (i : Π⦃c⦄, g c ≠ 0 → β) (hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
326 (j : Π⦃b⦄, f b ≠ 0 → γ) (hj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
327 (hji : ∀⦃c⦄ (h : g c ≠ 0), j (hi h) = c)
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
328 (hij : ∀⦃b⦄ (h : f b ≠ 0), i (hj h) = b)
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
329 (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
330 (∑i, f i) = (∑j, g j) :=
id ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
331 tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero i hi j hj hji hij hgj
id └─────────────────────────────────┘ ┴ └────────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ └─┘
src └─────────────────────────────────┘ └────────────────────────────┘
typ └─────────────────────────────────┘ ┴ └────────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘ └─┘
332
333 lemma tsum_eq_tsum_of_ne_zero_bij {f : β → α} {g : γ → α}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
334 (i : Π⦃c⦄, g c ≠ 0 → β)
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
335 (h₁ : ∀⦃c₁ c₂⦄ (h₁ : g c₁ ≠ 0) (h₂ : g c₂ ≠ 0), i h₁ = i h₂ → c₁ = c₂)
id └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘
336 (h₂ : ∀⦃b⦄, f b ≠ 0 → ∃c (h : g c ≠ 0), i h = b)
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
337 (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
338 (∑i, f i) = (∑j, g j) :=
id ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
339 tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero_bij i h₁ h₂ h₃
id └─────────────────────────────────┘ ┴ └────────────────────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────────────────────┘ └────────────────────────────────┘
typ └─────────────────────────────────┘ ┴ └────────────────────────────────┘ ┴ └┘ └┘ └┘
340
341 lemma tsum_eq_tsum_of_iso (j : γ → β) (i : β → γ)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
342 (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
343 (∑c, f (j c)) = (∑b, f b) :=
id ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
344 tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_iso i h₁ h₂
id └─────────────────────────────────┘ ┴ └────────────────────────┘ ┴ └┘ └┘
src └─────────────────────────────────┘ └────────────────────────┘
typ └─────────────────────────────────┘ ┴ └────────────────────────┘ ┴ └┘ └┘
345
346 lemma tsum_equiv (j : γ ≃ β) : (∑c, f (j c)) = (∑b, f b) :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴
347 tsum_eq_tsum_of_iso j j.symm (by simp) (by simp)
id └─────────────────┘ ┴ ┴└───┘
src └─────────────────┘ └───┘ └──┘ └──┘
typ └─────────────────┘ ┴ ┴└───┘ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
348
349 variable [topological_add_monoid α]
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
350
351 lemma tsum_add (hf : summable f) (hg : summable g) : (∑b, f b + g b) = (∑b, f b) + (∑b, g b) :=
id └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
352 tsum_eq_has_sum $ has_sum_add (has_sum_tsum hf) (has_sum_tsum hg)
id └─────────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
src └─────────────┘ └─────────┘ └──────────┘ └──────────┘
typ └─────────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
353
354 lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └────┘ └──────┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └────┘ └──────┘
355 (∑b, s.sum (λi, f i b)) = s.sum (λi, ∑b, f i b) :=
id ┴┴┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴┴┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
356 tsum_eq_has_sum $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
id └─────────────┘ └─────────┘ ┴ └┘ └──────────┘ └┘ ┴ └┘
src └─────────────┘ └─────────┘ └──────────┘
typ └─────────────┘ └─────────┘ ┴ └┘ └──────────┘ └┘ ┴ └┘
357
358 lemma tsum_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
id └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └───────────┘
359 (h₁ : ∀b, summable (λc, f ⟨b, c⟩)) (h₂ : summable f) : (∑p, f p) = (∑b c, f ⟨b, c⟩) :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴ ┴ ┴
360 (tsum_eq_has_sum $ has_sum_sigma (assume b, has_sum_tsum $ h₁ b) $ has_sum_tsum h₂).symm
id └─────────────┘ └───────────┘ ┴ └──────────┘ └┘ ┴ └──────────┘ └┘ └──┘
src └─────────────┘ └───────────┘ └──────────┘ └──────────┘ └──┘
typ └─────────────┘ └───────────┘ ┴ └──────────┘ └┘ ┴ └──────────┘ └┘ └──┘
361
362 end tsum
363
364 section topological_group
365 variables [add_comm_group α] [topological_space α] [topological_add_group α]
id └────────────┘ └───────────────┘ └───────────────────┘
src └────────────┘ └───────────────┘ └───────────────────┘
typ └────────────┘ └───────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
366 variables {f g : β → α} {a a₁ a₂ : α}
367
368 lemma has_sum_neg : has_sum f a → has_sum (λb, - f b) (- a) :=
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
369 has_sum_hom has_neg.neg continuous_neg
id └─────────┘ └─────────┘ └────────────┘
src └─────────┘ └─────────┘ └────────────┘
typ └─────────┘ └─────────┘ └────────────┘
370
371 lemma summable_neg (hf : summable f) : summable (λb, - f b) :=
id └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
372 summable_spec $ has_sum_neg $ has_sum_tsum $ hf
id └───────────┘ └─────────┘ └──────────┘ └┘
src └───────────┘ └─────────┘ └──────────┘
typ └───────────┘ └─────────┘ └──────────┘ └┘
373
374 lemma has_sum_sub (hf : has_sum f a₁) (hg : has_sum g a₂) : has_sum (λb, f b - g b) (a₁ - a₂) :=
id └─────┘ ┴ └┘ └─────┘ ┴ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
src └─────┘ └─────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
doc └─────┘ └─────┘ └─────┘
375 by simp; exact has_sum_add hf (has_sum_neg hg)
id └─────────┘ └┘ └─────────┘ └┘
src └──┘ └────┘└─────────┘┴ ┴ └─────────┘┴ └─
typ └──┘ └────┘└─────────┘┴└┘┴ └─────────┘┴└┘└─
doc └──┘ └────┘ ┴ ┴ ┴ └─
txt └──┘ └────┘ ┴ ┴ ┴ └─
par └──┘ └────┘ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ ┴└
st └────────────────────────────────────────────
376
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
377 lemma summable_sub (hf : summable f) (hg : summable g) : summable (λb, f b - g b) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
378 summable_spec $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
id └───────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
src └───────────┘ └─────────┘ └──────────┘ └──────────┘
typ └───────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
379
380 section tsum
381 variables [t2_space α]
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
382
383 lemma tsum_neg (hf : summable f) : (∑b, - f b) = - (∑b, f b) :=
id └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴
384 tsum_eq_has_sum $ has_sum_neg $ has_sum_tsum $ hf
id └─────────────┘ └─────────┘ └──────────┘ └┘
src └─────────────┘ └─────────┘ └──────────┘
typ └─────────────┘ └─────────┘ └──────────┘ └┘
385
386 lemma tsum_sub (hf : summable f) (hg : summable g) : (∑b, f b - g b) = (∑b, f b) - (∑b, g b) :=
id └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
387 tsum_eq_has_sum $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
id └─────────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
src └─────────────┘ └─────────┘ └──────────┘ └──────────┘
typ └─────────────┘ └─────────┘ └──────────┘ └┘ └──────────┘ └┘
388
389 lemma tsum_eq_zero_add {f : ℕ → α} (hf : summable f) : (∑b, f b) = f 0 + (∑b, f (b + 1)) :=
id ┴ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴
390 begin
st └─────
391 let f₁ : ℕ → α := λ n, nat.rec (f 0) (λ _ _, 0) n,
id ┴ └─────┘ ┴
src └───────┘ ┴ ┴ └──┘ └──┘└─────┘┴ └──┘ └───────┘
typ └───────┘ ┴ ┴┴└──┘ └──┘└─────┘┴ ┴└──┘ └───────┘
doc └───────┘ ┴ ┴ └──┘ └──┘ ┴ └──┘ └───────┘
txt └───────┘ ┴ ┴ └──┘ └──┘ ┴ └──┘ └───────┘
par └───────┘ ┴ ┴ └──┘ └──┘ ┴ └──┘ └───────┘
pid └────┘└─┘ ┴ ┴ └──┘ └──┘ ┴ └──┘ └───────┘
st ──────────────────────────────────────────────────┘└─
392 let f₂ : ℕ → α := λ n, nat.rec 0 (λ k _, f (k+1)) n,
id ┴ └─────┘ ┴ ┴
src └───────┘ ┴ ┴ └──┘ └──┘└─────┘└─┘ └────┘ ┴ ┴└──┘
typ └───────┘ ┴ ┴┴└──┘ └──┘└─────┘└─┘ └────┘┴┴ ┴└──┘
doc └───────┘ ┴ ┴ └──┘ └──┘ └─┘ └────┘ ┴ └──┘
txt └───────┘ ┴ ┴ └──┘ └──┘ └─┘ └────┘ ┴ └──┘
par └───────┘ ┴ ┴ └──┘ └──┘ └─┘ └────┘ ┴ └──┘
pid └────┘└─┘ ┴ ┴ └──┘ └──┘ └─┘ └────┘ ┴ └──┘
st ────────────────────────────────────────────────────┘└─
393 have : f = λ n, f₁ n + f₂ n, { ext n, symmetry, cases n, apply add_zero, apply zero_add },
id ┴ ┴ └┘ └┘ ┴ └──────┘ └──────┘
src └─────┘ ┴┴┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └──────┘ └────┘ └────┘└──────┘ └────┘└──────┘┴
typ └─────┘┴┴┴┴ └──┘└┘┴ ┴ ┴└┘┴ └───┘ └──────┘ └────┘┴ └────┘└──────┘ └────┘└──────┘┴
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └──────┘ └────┘ └────┘ └────┘ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └──────┘ └────┘ └────┘ └────┘ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └──────┘ └────┘ └────┘ └────┘ ┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ────────────────────────────┘└──┘└───┘└────────┘└───────┘└──────────────┘└───────────────┘└┘└
394 have hf₁ : summable f₁,
id └──────┘ └┘
src └─────────┘└──────┘┴
typ └─────────┘└──────┘┴└┘
doc └─────────┘└──────┘┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └──────┘└─┘ ┴
st ───────────────────────┘└─
395 { fapply summable_sum_of_ne_finset_zero,
id └────────────────────────────┘
src └─────┘└────────────────────────────┘
typ └─────┘└────────────────────────────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ───┘└───────────────────────────────────┘└─
396 { exact finset.singleton 0 },
id └──────────────┘
src └────┘└──────────────┘└─┘
typ └────┘└──────────────┘└─┘
doc └────┘└──────────────┘└─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ ┴└┘
st ─────┘└───────────────────────┘└┘└
397 { rintros (_ | n) hn,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ───────────────────────┘└─
398 { exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ───────┘└─────┘└─
399 apply hn,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────┘└─
400 apply finset.mem_singleton_self },
id └───────────────────────┘
src └────┘└───────────────────────┘┴
typ └────┘└───────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────┘└┘└
401 { refl } } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────┘└────┘└
402 have hf₂ : summable f₂,
id └──────┘ └┘
src └─────────┘└──────┘┴
typ └─────────┘└──────┘┴└┘
doc └─────────┘└──────┘┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └──────┘└─┘ ┴
st ───────────────────────┘└─
403 { have : f₂ = λ n, f n - f₁ n, ext, rw [eq_sub_iff_add_eq', this],
id └┘ ┴ ┴ └┘ └────────────────┘ └──┘
src └─────┘ ┴ ┴ └──┘ ┴ ┴┴┴ ┴ └─┘ └──┘└────────────────┘└┘ ┴
typ └─────┘└┘┴ ┴ └──┘┴┴ ┴┴┴└┘┴ └─┘ └──┘└────────────────┘└┘└──┘┴
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └──┘ └┘ ┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
st ───┘└─────────────────────────┘└───┘└──────────────────────┘└────┘└──
404 rw [this], apply summable_sub hf hf₁ },
id └──┘ └──────────┘ └┘ └─┘
src └──┘ ┴ └────┘└──────────┘┴ ┴ ┴
typ └──┘└──┘┴ └────┘└──────────┘┴└┘┴└─┘┴
doc └──┘ ┴ └────┘ ┴ ┴ ┴
txt └──┘ ┴ └────┘ ┴ ┴ ┴
par └──┘ ┴ └────┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴
st ───────────┘└───────────────────────────┘└┘└
405 conv_lhs { rw [this] },
id └──┘
src └─────────┘└──┘ └┘┴
typ └─────────┘└──┘└──┘└┘┴
txt └─────────┘└──┘ └┘┴
par └─────────┘└──┘ └┘┴
pid ┴└────┘ └─┘
st ───────────┘└───────┘ ┴└┘└
406 rw [tsum_add hf₁ hf₂, tsum_eq_single 0],
id └──────┘ └─┘ └─┘ └────────────┘
src └──┘└──────┘┴ ┴ └┘└────────────┘└─┘
typ └──┘└──────┘┴└─┘┴└─┘└┘└────────────┘└─┘
doc └──┘ ┴ ┴ └┘ └─┘
txt └──┘ ┴ ┴ └┘ └─┘
par └──┘ ┴ ┴ └┘ └─┘
pid └┘ ┴ ┴ └┘ └─┘
st ─────────────────────┘└───────────────┘└───
407 { congr' 1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ───┘└──────┘└─
408 fapply tsum_eq_tsum_of_ne_zero_bij (λ n _, n + 1),
id └─────────────────────────┘
src └─────┘└─────────────────────────┘┴ └────┘ ┴ └─┘
typ └─────┘└─────────────────────────┘┴ └────┘ ┴ └─┘
doc └─────┘ ┴ └────┘ ┴ └─┘
txt └─────┘ ┴ └────┘ ┴ └─┘
par └─────┘ ┴ └────┘ ┴ └─┘
pid ┴ ┴ └────┘ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
409 { intros _ _ _ _, exact nat.succ_inj },
id └──────────┘
src └────────────┘ └────┘└──────────┘┴
typ └────────────┘ └────┘└──────────┘┴
doc └────────────┘ └────┘ ┴
txt └────────────┘ └────┘ ┴
par └────────────┘ └────┘ ┴
pid └──────┘ ┴ ┴
st ─────┘└────────────┘└───────────────────┘└┘└
410 { rintros (_ | n) h,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ─────┘└───────────────┘└─
411 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────┘└────────────┘└┘└
412 { exact ⟨n, h, rfl⟩ } },
id ┴ ┴ └─┘
src └────┘ └┘ └┘└─┘└┘
typ └────┘ ┴└┘┴└┘└─┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ─────────────────────────┘└──┘└
413 { intros, refl },
src └────┘ └───┘
typ └────┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴
st ─────┘└────┘└─────┘└┘└
414 { apply_instance } },
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st ────────────────────┘└──┘└
415 { rintros (_ | n) hn,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ───┘└────────────────┘└─
416 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────┘└────────────┘└┘└
417 { refl } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└──┘└
418 { apply_instance }
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st ──────────────────┘└─
419 end
st ──┘
420
421 end tsum
422
423 end topological_group
424
425 section topological_semiring
426 variables [semiring α] [topological_space α] [topological_semiring α]
id └──────┘ └───────────────┘ └──────────────────┘
src └──────┘ └───────────────┘ └──────────────────┘
typ └──────┘ └───────────────┘ └──────────────────┘
doc └───────────────┘ └──────────────────┘
427 variables {f g : β → α} {a a₁ a₂ : α}
428
429 lemma has_sum_mul_left (a₂) : has_sum f a₁ → has_sum (λb, a₂ * f b) (a₂ * a₁) :=
id └─────┘ ┴ └┘ └─────┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘
src └─────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ └┘ └─────┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘
doc └─────┘ └─────┘
430 has_sum_hom _ (continuous_const.mul continuous_id)
id └─────────┘ └──────────────┘└──┘ └───────────┘
src └─────────┘ └──────────────┘└──┘ └───────────┘
typ └─────────┘ └──────────────┘└──┘ └───────────┘
431
432 lemma has_sum_mul_right (a₂) (hf : has_sum f a₁) : has_sum (λb, f b * a₂) (a₁ * a₂) :=
id └─────┘ ┴ └┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘
src └─────┘ └─────┘ ┴ ┴
typ └─────┘ ┴ └┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘
doc └─────┘ └─────┘
433 @has_sum_hom _ _ _ _ _ f a₁ (λa, a * a₂) _ _ _
id └─────────┘ ┴ └┘ ┴ ┴ ┴ └┘
src └─────────┘ ┴
typ └─────────┘ ┴ └┘ ┴ ┴ ┴ └┘
434 (continuous_id.mul continuous_const) hf
id └───────────┘└──┘ └──────────────┘ └┘
src └───────────┘└──┘ └──────────────┘
typ └───────────┘└──┘ └──────────────┘ └┘
435
436 lemma summable_mul_left (a) (hf : summable f) : summable (λb, a * f b) :=
id └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
437 summable_spec $ has_sum_mul_left _ $ has_sum_tsum hf
id └───────────┘ └──────────────┘ └──────────┘ └┘
src └───────────┘ └──────────────┘ └──────────┘
typ └───────────┘ └──────────────┘ └──────────┘ └┘
438
439 lemma summable_mul_right (a) (hf : summable f) : summable (λb, f b * a) :=
id └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
440 summable_spec $ has_sum_mul_right _ $ has_sum_tsum hf
id └───────────┘ └───────────────┘ └──────────┘ └┘
src └───────────┘ └───────────────┘ └──────────┘
typ └───────────┘ └───────────────┘ └──────────┘ └┘
441
442 section tsum
443 variables [t2_space α]
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
444
445 lemma tsum_mul_left (a) (hf : summable f) : (∑b, a * f b) = a * (∑b, f b) :=
id └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴
446 tsum_eq_has_sum $ has_sum_mul_left _ $ has_sum_tsum hf
id └─────────────┘ └──────────────┘ └──────────┘ └┘
src └─────────────┘ └──────────────┘ └──────────┘
typ └─────────────┘ └──────────────┘ └──────────┘ └┘
447
448 lemma tsum_mul_right (a) (hf : summable f) : (∑b, f b * a) = (∑b, f b) * a :=
id └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴
449 tsum_eq_has_sum $ has_sum_mul_right _ $ has_sum_tsum hf
id └─────────────┘ └───────────────┘ └──────────┘ └┘
src └─────────────┘ └───────────────┘ └──────────┘
typ └─────────────┘ └───────────────┘ └──────────┘ └┘
450
451 end tsum
452
453 end topological_semiring
454
455 section order_topology
456 variables [ordered_comm_monoid α] [topological_space α] [order_closed_topology α]
id ┴└─────────────────┘ ┴└───────────────┘ └───────────────────┘
src └─────────────────┘ └───────────────┘ └───────────────────┘
typ ┴└─────────────────┘ ┴└───────────────┘ └───────────────────┘
doc └─────────────────┘ └───────────────┘ └───────────────────┘
457 variables {f g : β → α} {a a₁ a₂ : α}
458
459 lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘
src ┴ └─────┘ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘
doc └─────┘ └─────┘
460 le_of_tendsto_of_tendsto at_top_ne_bot hf hg $ univ_mem_sets' $
id └──────────────────────┘ └───────────┘ └┘ └┘ └────────────┘
src └──────────────────────┘ └───────────┘ └────────────┘
typ └──────────────────────┘ └───────────┘ └┘ └┘ └────────────┘
461 assume s, sum_le_sum $ assume b _, h b
id ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴
462
463 lemma has_sum_le_inj {g : γ → α} (i : β → γ) (hi : injective i) (hs : ∀c∉set.range i, 0 ≤ g c)
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
464 (h : ∀b, f b ≤ g (i b)) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘
src ┴ └─────┘ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ └─────┘ ┴ └┘ └┘ ┴ └┘
doc └─────┘ └─────┘
465 have has_sum (λc, (partial_inv i c).cases_on' 0 f) a₁,
id └─────┘ ┴ └─────────┘ ┴ ┴ └───────┘ ┴ └┘
src └─────┘ └─────────┘ └───────┘
typ └─────┘ ┴ └─────────┘ ┴ ┴ └───────┘ ┴ └┘
doc └─────┘ └─────────┘
466 begin
st └─────
467 refine (has_sum_iff_has_sum_of_ne_zero_bij (λb _, i b) _ _ _).2 hf,
id └────────────────────────────────┘ ┴ └┘
src └─────┘ └────────────────────────────────┘┴ └───┘ ┴ └─────────┘
typ └─────┘ └────────────────────────────────┘┴ └───┘┴┴ └─────────┘└┘
doc └─────┘ ┴ └───┘ ┴ └─────────┘
txt └─────┘ ┴ └───┘ ┴ └─────────┘
par └─────┘ ┴ └───┘ ┴ └─────────┘
pid ┴ ┴ └───┘ ┴ └─────────┘
st ───────────────────────────────────────────────────────────────────┘└─
468 { assume c₁ c₂ h₁ h₂ eq, exact hi eq },
id └┘ └┘
src └───────────────────┘ └────┘ ┴└┘┴
typ └───────────────────┘ └────┘└┘┴└┘┴
doc └───────────────────┘ └────┘ ┴ ┴
txt └───────────────────┘ └────┘ ┴ ┴
par └───────────────────┘ └────┘ ┴ ┴
pid └───────────────────┘ ┴ ┴ ┴
st ───┘└───────────────────┘└────────────┘└┘└
469 { assume c hc,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
470 cases eq : partial_inv i c with b; rw eq at hc,
id └─────────┘ ┴ ┴ └┘
src └────┘ └─┘└─────────┘┴ ┴ └─────┘ └─┘└┘└────┘
typ └────┘ └─┘└─────────┘┴┴┴┴└─────┘ └─┘└┘└────┘
doc └────┘ └─┘└─────────┘┴ ┴ └─────┘ └─┘ └────┘
txt └────┘ └─┘ ┴ ┴ └─────┘ └─┘ └────┘
par └────┘ └─┘ ┴ ┴ └─────┘ └─┘ └────┘
pid ┴ └─┘ ┴ ┴ └─────┘ ┴ └────┘
st ─────────────────────────────────────────┘└┘└────┘└─
471 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────┘└────────────┘└┘└
472 { rw [partial_inv_of_injective hi] at eq,
id └──────────────────────┘ └┘
src └──┘└──────────────────────┘┴ └─────┘
typ └──┘└──────────────────────┘┴└┘└─────┘
doc └──┘ ┴ └─────┘
txt └──┘ ┴ └─────┘
par └──┘ ┴ └─────┘
pid └┘ ┴ ┴└────┘
st ────────────────────────────────────┘┴└────┘└─
473 exact ⟨b, hc, eq⟩ } },
id ┴ └┘ └┘
src └────┘ └┘ └┘└┘└┘
typ └────┘ ┴└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ───────────────────────┘└──┘└
474 { assume c hc, rw [partial_inv_left hi, option.cases_on'] }
id └──────────────┘ └┘ └──────────────┘
src └─────────┘ └──┘└──────────────┘┴ └┘└──────────────┘└┘
typ └─────────┘ └──┘└──────────────┘┴└┘└┘└──────────────┘└┘
doc └─────────┘ └──┘ ┴ └┘ └┘
txt └─────────┘ └──┘ ┴ └┘ └┘
par └─────────┘ └──┘ ┴ └┘ └┘
pid └─────────┘ └┘ ┴ └┘ ┴┴
st ──────────────┘└───────────────────────┘└────────────────┘┴┴└─
475 end,
st ──┘
476 begin
st └─────
477 refine has_sum_le (assume c, _) this hg,
id └────────┘ └──┘ └┘
src └─────┘└────────┘┴ └─────┘ ┴
typ └─────┘└────────┘┴ └─────┘└──┘┴└┘
doc └─────┘ ┴ └─────┘ ┴
txt └─────┘ ┴ └─────┘ ┴
par └─────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ────────────────────────────────────────┘└─
478 by_cases c ∈ set.range i,
id ┴ ┴ └───────┘ ┴
src └───────┘ ┴┴┴└───────┘┴
typ └───────┘┴┴┴┴└───────┘┴┴
doc └───────┘ ┴ ┴└───────┘┴
txt └───────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────┘└─
479 { rcases h with ⟨b, rfl⟩,
id ┴
src └─────┘ └────────────┘
typ └─────┘┴└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ───┘└────────────────────┘└─
480 rw [partial_inv_left hi, option.cases_on'],
id └──────────────┘ └┘ └──────────────┘
src └──┘└──────────────┘┴ └┘└──────────────┘┴
typ └──┘└──────────────┘┴└┘└┘└──────────────┘┴
doc └──┘ ┴ └┘ ┴
txt └──┘ ┴ └┘ ┴
par └──┘ ┴ └┘ ┴
pid └┘ ┴ └┘ ┴
st ──────────────────────────┘└────────────────┘└──
481 exact h _ },
id ┴
src └────┘ └─┘
typ └────┘┴└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────┘└┘└
482 { have : partial_inv i c = none := dif_neg h,
id └─────────┘ ┴ ┴ └──┘ └─────┘ ┴
src └─────┘└─────────┘┴ ┴ ┴ ┴└──┘└──┘└─────┘┴
typ └─────┘└─────────┘┴┴┴┴┴ ┴└──┘└──┘└─────┘┴┴
doc └─────┘└─────────┘┴ ┴ ┴ ┴ └──┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────┘└─
483 rw [this, option.cases_on'],
id └──┘ └──────────────┘
src └──┘ └┘└──────────────┘┴
typ └──┘└──┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────┘└────────────────┘└──
484 exact hs _ h }
id └┘ ┴
src └────┘ └─┘ ┴
typ └────┘└┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────┘└─
485 end
st ──┘
486
487 lemma sum_le_has_sum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : has_sum f a) :
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
src └────┘ ┴ └─────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └────┘ └─────┘
488 s.sum f ≤ a :=
id ┴└──┘ ┴ ┴ ┴
src └──┘ ┴
typ ┴└──┘ ┴ ┴ ┴
489 ge_of_tendsto at_top_ne_bot hf (mem_at_top_sets.2 ⟨s, λ t hst,
id └───────────┘ └───────────┘ └┘ └─────────────┘┴ ┴ ┴ └─┘
src └───────────┘ └───────────┘ └─────────────┘┴
typ └───────────┘ └───────────┘ └┘ └─────────────┘┴ ┴ ┴ └─┘
490 sum_le_sum_of_subset_of_nonneg hst $ λ b hbt hbs, hs b hbs⟩)
id └────────────────────────────┘ └─┘ ┴ └─┘ └─┘ └┘ ┴ └─┘
src └────────────────────────────┘
typ └────────────────────────────┘ └─┘ ┴ └─┘ └─┘ └┘ ┴ └─┘
491
492 lemma sum_le_tsum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : summable f) :
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src └────┘ ┴ └──────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └────┘ └──────┘
493 s.sum f ≤ tsum f :=
id ┴└──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ ┴└──┘ ┴ ┴ └──┘ ┴
doc └──┘
494 sum_le_has_sum s hs (has_sum_tsum hf)
id └────────────┘ ┴ └┘ └──────────┘ └┘
src └────────────┘ └──────────┘
typ └────────────┘ ┴ └┘ └──────────┘ └┘
495
496 lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : summable f) (hg : summable g) : (∑b, f b) ≤ (∑b, g b) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ └──────┘ └──────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴ ┴ ┴
497 has_sum_le h (has_sum_tsum hf) (has_sum_tsum hg)
id └────────┘ ┴ └──────────┘ └┘ └──────────┘ └┘
src └────────┘ └──────────┘ └──────────┘
typ └────────┘ ┴ └──────────┘ └┘ └──────────┘ └┘
498
499 end order_topology
500
501 section uniform_group
502
503 variables [add_comm_group α] [uniform_space α] [complete_space α]
id └────────────┘ ┴└───────────┘ └────────────┘
src └────────────┘ └───────────┘ └────────────┘
typ └────────────┘ ┴└───────────┘ └────────────┘
doc └───────────┘ └────────────┘
504 variables (f g : β → α) {a a₁ a₂ : α}
505
506 lemma summable_iff_cauchy : summable f ↔ cauchy (map (λ (s : finset β), sum s f) at_top) :=
id └──────┘ ┴ ┴ └────┘ └─┘ └────┘ ┴ └─┘ ┴ ┴ └────┘
src └──────┘ ┴ └────┘ └─┘ └────┘ └─┘ └────┘
typ └──────┘ ┴ ┴ └────┘ └─┘ └────┘ ┴ └─┘ ┴ ┴ └────┘
doc └──────┘ └────┘ └─┘ └────┘ └────┘
507 (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm
id └───────────────────────────┘ └───────────┘ └──┘
src └───────────────────────────┘ └───────────┘ └──┘
typ └───────────────────────────┘ └───────────┘ └──┘
508
509 variable [uniform_add_group α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
510
511 lemma summable_iff_vanishing :
512 summable f ↔ ∀ e ∈ 𝓝 (0:α), (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴┴ ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ └────┘ ┴ └──────┘ └──┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴┴ ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴
doc └──────┘ ┴ └────┘ └──────┘
513 begin
st └─────
514 simp only [summable_iff_cauchy, cauchy_map_iff, and_iff_right at_top_ne_bot,
id └─────────────────┘ └────────────┘ └───────────┘ └───────────┘
src └─────────┘└─────────────────┘└┘└────────────┘└┘└───────────┘┴└───────────┘└─
typ └─────────┘└─────────────────┘└┘└────────────┘└┘└───────────┘┴└───────────┘└─
doc └─────────┘ └┘ └┘ ┴ └─
txt └─────────┘ └┘ └┘ ┴ └─
par └─────────┘ └┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ └┘ ┴ └─
st ───────────────────────────────────────────────────────────────────────────────
515 prod_at_top_at_top_eq, uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (∘)],
id └───────────────────┘ └───────────────────────────┘ ┴ └───────────────┘ ┴
src ───┘└───────────────────┘└┘└───────────────────────────┘┴ └┘└───────────────┘└┘┴└─┘
typ ───┘└───────────────────┘└┘└───────────────────────────┘┴┴└┘└───────────────┘└┘┴└─┘
doc ───┘ └┘ ┴ └┘ └┘ └─┘
txt ───┘ └┘ ┴ └┘ └┘ └─┘
par ───┘ └┘ ┴ └┘ └┘ └─┘
pid ───┘ └┘ ┴ └┘ └┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
516 rw [tendsto_at_top' (_ : finset β × finset β → α)],
id └─────────────┘ ┴ └────┘ ┴ ┴
src └──┘└─────────────┘┴ └──┘ ┴ ┴┴┴└────┘┴ ┴ ┴ └┘
typ └──┘└─────────────┘┴ └──┘ ┴ ┴┴┴└────┘┴┴┴ ┴┴└┘
doc └──┘ ┴ └──┘ ┴ ┴ ┴└────┘┴ ┴ ┴ └┘
txt └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────┘└──
517 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
518 { assume h e he,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ───┘└───────────┘└─
519 rcases h e he with ⟨⟨s₁, s₂⟩, h⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └─────────────────┘
typ └─────┘┴┴┴┴└┘└─────────────────┘
doc └─────┘ ┴ ┴ └─────────────────┘
txt └─────┘ ┴ ┴ └─────────────────┘
par └─────┘ ┴ ┴ └─────────────────┘
pid ┴ ┴ ┴ └─────────────────┘
st ───────────────────────────────────┘└─
520 use [s₁ ∪ s₂],
id └┘ ┴ └┘
src └───┘ ┴┴┴ ┴
typ └───┘└┘┴┴┴└┘┴
doc └───┘ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st ────────────────┘└─
521 assume t ht,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
522 specialize h (s₁ ∪ s₂, (s₁ ∪ s₂) ∪ t) ⟨le_sup_left, le_sup_left_of_le le_sup_right⟩,
id ┴ ┴ └┘ └┘ ┴ └─────────┘ └───────────────┘ └──────────┘
src └─────────┘ ┴┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └─────────┘└┘└───────────────┘┴└──────────┘┴
typ └─────────┘┴┴┴ ┴ ┴ └┘ └┘┴ ┴└┘└┘ ┴┴└┘ └─────────┘└┘└───────────────┘┴└──────────┘┴
doc └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ ┴ ┴
par └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
523 simpa only [finset.sum_union ht.symm, add_sub_cancel'] using h },
id └──────────────┘ └─────┘ └─────────────┘ ┴
src └──────────┘└──────────────┘┴└─────┘└┘└─────────────┘└──────┘ ┴
typ └──────────┘└──────────────┘┴└─────┘└┘└─────────────┘└──────┘┴┴
doc └──────────┘ ┴ └┘ └──────┘ ┴
txt └──────────┘ ┴ └┘ └──────┘ ┴
par └──────────┘ ┴ └┘ └──────┘ ┴
pid ┴└──┘└┘ ┴ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────────────┘└┘└
524 { assume h e he,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ────────────────┘└─
525 rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩,
id └──────────────────┘ └┘
src └─────┘└──────────────────┘┴ └────────────────┘
typ └─────┘└──────────────────┘┴└┘└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ───────────────────────────────────────────────────┘└─
526 rcases h d hd with ⟨s, h⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └──────────┘
typ └─────┘┴┴┴┴└┘└──────────┘
doc └─────┘ ┴ ┴ └──────────┘
txt └─────┘ ┴ ┴ └──────────┘
par └─────┘ ┴ ┴ └──────────┘
pid ┴ ┴ ┴ └──────────┘
st ────────────────────────────┘└─
527 use [(s, s)],
id ┴
src └───┘ └┘ └┘
typ └───┘ └┘┴└┘
doc └───┘ └┘ └┘
txt └───┘ └┘ └┘
par └───┘ └┘ └┘
pid └┘ └┘ └┘
st ───────────────┘└─
528 rintros ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └──────────────────┘
st ──────────────────────────────┘└─
529 have : t₂.sum f - t₁.sum f = (t₂ \ s).sum f - (t₁ \ s).sum f,
id └────┘ ┴ └────┘ ┴ └┘ ┴ └┘ ┴ ┴
src └─────┘└────┘┴ ┴┴┴└────┘┴ ┴┴┴ ┴┴┴ └────┘ ┴ ┴ ┴ ┴ └────┘
typ └─────┘└────┘┴ ┴┴┴└────┘┴ ┴┴┴ └┘┴┴┴ └────┘ ┴ ┴ └┘┴ ┴┴└────┘┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
st ───────────────────────────────────────────────────────────────┘└─
530 { simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
id └──────────────┘ └─┘ └──────────────┘ └─┘
src └─────────┘ └──────────────┘┴ └──────┘ └──────────────┘┴ └───────
typ └─────────┘ └──────────────┘┴└─┘└──────┘ └──────────────┘┴└─┘└───────
doc └─────────┘ ┴ └──────┘ ┴ └───────
txt └─────────┘ ┴ └──────┘ ┴ └───────
par └─────────┘ ┴ └──────┘ ┴ └───────
pid ┴└──┘└┘ ┴ └──────┘ ┴ └───────
st ─────┘└────────────────────────────────────────────────────────────────────
531 add_sub_add_right_eq_sub] },
id └──────────────────────┘
src ───────┘└──────────────────────┘└┘
typ ───────┘└──────────────────────┘└┘
doc ───────┘ └┘
txt ───────┘ └┘
par ───────┘ └┘
pid ───────┘ ┴┴
st ─────────────────────────────────┘└┘└
532 simp only [this],
id └──┘
src └─────────┘ ┴
typ └─────────┘└──┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───────────────────┘└─
533 exact hde _ _ (h _ finset.sdiff_disjoint) (h _ finset.sdiff_disjoint) }
id └─┘ ┴ └───────────────────┘
src └────┘ └───┘ └─┘ └┘ └─┘└───────────────────┘└┘
typ └────┘└─┘└───┘ └─┘ └┘ ┴└─┘└───────────────────┘└┘
doc └────┘ └───┘ └─┘ └┘ └─┘ └┘
txt └────┘ └───┘ └─┘ └┘ └─┘ └┘
par └────┘ └───┘ └─┘ └┘ └─┘ └┘
pid ┴ └───┘ └─┘ └┘ └─┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────┘└─
534 end
st ──┘
535
536 /- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -/
537 lemma summable_of_summable_of_sub (hf : summable f) (h : ∀b, g b = 0 ∨ g b = f b) : summable g :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
538 (summable_iff_vanishing g).2 $
id └────────────────────┘ ┴ ┴
src └────────────────────┘ ┴
typ └────────────────────┘ ┴ ┴
539 assume e he,
id ┴ └┘
typ ┴ └┘
540 let ⟨s, hs⟩ := (summable_iff_vanishing f).1 hf e he in
id └─┘ ┴ └┘ └────────────────────┘ ┴ ┴ └┘ ┴ └┘
src └────────────────────┘ ┴
typ └─┘ ┴ └┘ └────────────────────┘ ┴ ┴ └┘ ┴ └┘
541 ⟨s, assume t ht,
id ┴ └┘
typ ┴ └┘
542 have eq : (t.filter (λb, g b = f b)).sum f = t.sum g :=
id ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴
src └─────┘ ┴ └─┘ ┴ └──┘
typ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴
doc └─────┘
543 calc (t.filter (λb, g b = f b)).sum f = (t.filter (λb, g b = f b)).sum g :
id ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘ └─────┘ ┴ └─┘
typ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─────┘ └─────┘
544 finset.sum_congr rfl (assume b hb, (finset.mem_filter.1 hb).2.symm)
id └──────────────┘ └─┘ ┴ └┘ └───────────────┘┴ └┘ ┴ └──┘
src └──────────────┘ └─┘ └───────────────┘┴ ┴ └──┘
typ └──────────────┘ └─┘ ┴ └┘ └───────────────┘┴ └┘ ┴ └──┘
545 ... = t.sum g :
id ┴└──┘ ┴
src └──┘
typ ┴└──┘ ┴
546 begin
st └─────
547 refine finset.sum_subset (finset.filter_subset _) _,
id └───────────────┘ └──────────────────┘
src └─────┘└───────────────┘┴ └──────────────────┘└───┘
typ └─────┘└───────────────┘┴ └──────────────────┘└───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ────────────────────────────────────────────────────────────┘└─
548 assume b hbt hb,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ────────────────────────┘└─
549 simp only [(∉), finset.mem_filter, and_iff_right hbt] at hb,
id ┴ └───────────────┘ └───────────┘ └─┘
src └─────────┘┴└──┘└───────────────┘└┘└───────────┘┴ └─────┘
typ └─────────┘┴└──┘└───────────────┘└┘└───────────┘┴└─┘└─────┘
doc └─────────┘ └──┘ └┘ ┴ └─────┘
txt └─────────┘ └──┘ └┘ ┴ └─────┘
par └─────────┘ └──┘ └┘ ┴ └─────┘
pid ┴└──┘└┘ └──┘ └┘ ┴ ┴┴└───┘
st ────────────────────────────────────────────────────────────────────┘└─
550 exact (h b).resolve_right hb
id ┴ ┴ └┘
src └────┘ ┴ └──────────────┘ └
typ └────┘ ┴┴┴└──────────────┘└┘└
doc └────┘ ┴ └──────────────┘ └
txt └────┘ ┴ └──────────────┘ └
par └────┘ ┴ └──────────────┘ └
pid ┴ ┴ └──────────────┘ └
st ───────────────────────────────────────
551 end,
src ───────┘
typ ───────┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘└─┘
552 eq ▸ hs _ $ finset.disjoint_of_subset_left (finset.filter_subset _) ht⟩
id └┘ ┴ └────────────────────────────┘ └──────────────────┘ └┘
src └┘ ┴ └────────────────────────────┘ └──────────────────┘
typ └┘ ┴ └────────────────────────────┘ └──────────────────┘ └┘
553
554 lemma summable_comp_of_summable_of_injective {i : γ → β} (hf : summable f) (hi : injective i) :
id ┴ ┴ └──────┘ ┴ └───────┘ ┴
src └──────┘ └───────┘
typ ┴ ┴ └──────┘ ┴ └───────┘ ┴
doc └──────┘
555 summable (f ∘ i) :=
id └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴
doc └──────┘
556 suffices summable (λb, if b ∈ set.range i then f b else 0),
id └──────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └──────┘ ┴ └───────┘
typ └──────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └──────┘ └───────┘
557 begin
st └─────
558 refine (summable_iff_summable_ne_zero_bij (λc _, i c) _ _ _).1 this,
id └───────────────────────────────┘ ┴ └──┘
src └─────┘ └───────────────────────────────┘┴ └───┘ ┴ └─────────┘
typ └─────┘ └───────────────────────────────┘┴ └───┘┴┴ └─────────┘└──┘
doc └─────┘ ┴ └───┘ ┴ └─────────┘
txt └─────┘ ┴ └───┘ ┴ └─────────┘
par └─────┘ ┴ └───┘ ┴ └─────────┘
pid ┴ ┴ └───┘ ┴ └─────────┘
st ────────────────────────────────────────────────────────────────────┘└─
559 { assume c₁ c₂ hc₁ hc₂ eq, exact hi eq },
id └┘ └┘
src └─────────────────────┘ └────┘ ┴└┘┴
typ └─────────────────────┘ └────┘└┘┴└┘┴
doc └─────────────────────┘ └────┘ ┴ ┴
txt └─────────────────────┘ └────┘ ┴ ┴
par └─────────────────────┘ └────┘ ┴ ┴
pid └─────────────────────┘ ┴ ┴ ┴
st ───┘└─────────────────────┘└────────────┘└┘└
560 { assume b hb,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
561 split_ifs at hb,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └────┘
st ──────────────────┘└─
562 { rcases h with ⟨c, rfl⟩,
id ┴
src └─────┘ └────────────┘
typ └─────┘┴└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ─────┘└────────────────────┘└─
563 exact ⟨c, hb, rfl⟩ },
id ┴ └┘ └─┘
src └────┘ └┘ └┘└─┘└┘
typ └────┘ ┴└┘└┘└┘└─┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ────────────────────────┘└┘└
564 { contradiction } },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────────┘└──┘└
565 { assume c hc, exact if_pos (set.mem_range_self _) }
id └────┘ └────────────────┘
src └─────────┘ └────┘└────┘┴ └────────────────┘└──┘
typ └─────────┘ └────┘└────┘┴ └────────────────┘└──┘
doc └─────────┘ └────┘ ┴ └──┘
txt └─────────┘ └────┘ ┴ └──┘
par └─────────┘ └────┘ ┴ └──┘
pid └─────────┘ ┴ ┴ └─┘┴
st ──────────────┘└────────────────────────────────────┘└─
566 end,
st ──┘
567 summable_of_summable_of_sub _ _ hf $ assume b, by by_cases b ∈ set.range i; simp [h]
id └─────────────────────────┘ └┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └─────────────────────────┘ └───────┘ ┴┴┴└───────┘┴ └────┘ └─
typ └─────────────────────────┘ └┘ ┴ └───────┘┴┴┴┴└───────┘┴┴ └────┘┴└─
doc └───────┘ ┴ ┴└───────┘┴ └────┘ └─
txt └───────┘ ┴ ┴ ┴ └────┘ └─
par └───────┘ ┴ ┴ ┴ └────┘ └─
pid ┴ ┴ ┴ ┴ ┴┴ ┴└
st └───────────────────────────────────
568
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
569 end uniform_group
570
571 section cauchy_seq
572 open finset.Ico filter
573
574 /-- If the extended distance between consequent points of a sequence is estimated
575 by a summable series of `nnreal`s, then the original sequence is a Cauchy sequence. -/
576 lemma cauchy_seq_of_edist_le_of_summable [emetric_space α] {f : ℕ → α} (d : ℕ → nnreal)
id └───────────┘ ┴ ┴ ┴ ┴ └────┘
src └───────────┘ ┴ ┴ └────┘
typ └───────────┘ ┴ ┴ ┴ ┴ └────┘
doc └───────────┘ └────┘
577 (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
id ┴ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴
src └───┘ └───┘ ┴ └──────┘ └────────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴
doc └──────┘ └────────┘
578 begin
st └─────
579 refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _),
id └───────────────────────────┘
src └─────┘└───────────────────────────┘└─┘ └─────────┘
typ └─────┘└───────────────────────────┘└─┘ └─────────┘
doc └─────┘└───────────────────────────┘└─┘ └─────────┘
txt └─────┘ └─┘ └─────────┘
par └─────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ─────────────────────────────────────────────────────┘└─
580 -- Actually we need partial sums of `d` to be a Cauchy sequence
st ──────────────────────────────────────────────────────────────────
581 replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
id └────────┘ └─┘ └───┘ ┴
src └───────────┘└────────┘┴ └────┘ └─┘└─┘┴ └───┘┴ └┘ └────
typ └───────────┘└────────┘┴ └────┘ └─┘└─┘┴ └───┘┴ └┘┴└────
doc └───────────┘└────────┘┴ └────┘ └─┘ ┴ └───┘┴ └┘ └────
txt └───────────┘ ┴ └────┘ └─┘ ┴ ┴ └┘ └────
par └───────────┘ ┴ └────┘ └─┘ ┴ ┴ └┘ └────
pid └─┘└─┘ ┴ └────┘ └─┘ ┴ ┴ └┘ ┴└───
st ──────────────────────────────────────────────────────────
582 let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
id ┴ └┘ └────────────────────────┘ └────────────────────────┘
src ───┘ ┴ └─┘ └───┘ └──┘└────────────────────────┘└─┘ └────────────────────────┘┴ ┴
typ ───┘ ┴ └─┘┴└───┘└┘└──┘└────────────────────────┘└─┘ └────────────────────────┘┴ ┴
doc ───┘ ┴ └─┘ └───┘ └──┘ └─┘ └────────────────────────┘┴ ┴
txt ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
par ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
pid ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
583 -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
st ────────────────────────────────────────────────────────────────────────────────
584 refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _),
id └────────────────────┘ └┘ ┴ └────────────┘ └──┘
src └─────┘ └────────────────────┘└─┘ ┴ ┴ └────────────┘└─┘ └─────┘ └────────────┘
typ └─────┘ └────────────────────┘└─┘└┘┴┴┴ └────────────┘└─┘└──┘└─────┘ └────────────┘
doc └─────┘ └────────────────────┘└─┘ ┴ ┴ └─┘ └─────┘ └────────────┘
txt └─────┘ └─┘ ┴ ┴ └─┘ └─────┘ └────────────┘
par └─────┘ └─┘ ┴ ┴ └─┘ └─────┘ └────────────┘
pid ┴ └─┘ ┴ ┴ └─┘ └─────┘ └────────────┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
585 have hsum := hN n hn,
id └┘ ┴ └┘
src └───────────┘ ┴ ┴
typ └───────────┘└┘┴┴┴└┘
doc └───────────┘ ┴ ┴
txt └───────────┘ ┴ ┴
par └───────────┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴
st ─────────────────────┘└─
586 -- We simplify the known inequality
st ──────────────────────────────────────
587 rw [dist_nndist, nnreal.nndist_eq, ← sum_range_add_sum_Ico _ hn, nnreal.add_sub_cancel'] at hsum,
id └─────────┘ └──────────────┘ └───────────────────┘ └┘ └────────────────────┘
src └──┘└─────────┘└┘└──────────────┘└──┘└───────────────────┘└─┘ └┘└────────────────────┘└───────┘
typ └──┘└─────────┘└┘└──────────────┘└──┘└───────────────────┘└─┘└┘└┘└────────────────────┘└───────┘
doc └──┘└─────────┘└┘ └──┘ └─┘ └┘ └───────┘
txt └──┘ └┘ └──┘ └─┘ └┘ └───────┘
par └──┘ └┘ └──┘ └─┘ └┘ └───────┘
pid └┘ └┘ └──┘ └─┘ └┘ ┴└──────┘
st ────────────────┘└────────────────┘└────────────────────────────┘└──────────────────────┘┴└──────┘└─
588 norm_cast at hsum,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └──────┘
st ──────────────────┘└─
589 replace hsum := lt_of_le_of_lt (le_max_left _ _) hsum,
id └────────────┘ └─────────┘ └──┘
src └──────────────┘└────────────┘┴ └─────────┘└────┘
typ └──────────────┘└────────────┘┴ └─────────┘└────┘└──┘
doc └──────────────┘ ┴ └────┘
txt └──────────────┘ ┴ └────┘
par └──────────────┘ ┴ └────┘
pid └───┘┴└─┘ ┴ └────┘
st ──────────────────────────────────────────────────────┘└─
590
st ─
591 -- Then use `hf` to simplify the goal to the same form
st ─────────────────────────────────────────────────────────
592 apply lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn (λ k _ _, hf k)),
id └────────────┘ └──────────────────────────┘ └┘ └┘
src └────┘└────────────┘┴ └──────────────────────────┘┴ ┴ └──────┘ ┴ └┘
typ └────┘└────────────┘┴ └──────────────────────────┘┴└┘┴ └──────┘└┘┴ └┘
doc └────┘ ┴ └──────────────────────────┘┴ ┴ └──────┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ └──────┘ ┴ └┘
par └────┘ ┴ ┴ ┴ └──────┘ ┴ └┘
pid ┴ ┴ ┴ ┴ └──────┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────┘└─
593 assumption_mod_cast
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid ┴
st ─────────────────────┘
594 end
st └─┘
595
596 /-- If the distance between consequent points of a sequence is estimated by a summable series,
597 then the original sequence is a Cauchy sequence. -/
598 lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
599 (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
id ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴
src └──┘ └───┘ ┴ └──────┘ └────────┘
typ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴
doc └──────┘ └────────┘
600 begin
st └─────
601 refine metric.cauchy_seq_iff'.2 (λε εpos, _),
id └────────────────────┘
src └─────┘└────────────────────┘└─┘ └────────┘
typ └─────┘└────────────────────┘└─┘ └────────┘
doc └─────┘└────────────────────┘└─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ─────────────────────────────────────────────┘└─
602 replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
id └────────┘ └─┘ └───┘ ┴
src └───────────┘└────────┘┴ └────┘ └─┘└─┘┴ └───┘┴ └┘ └────
typ └───────────┘└────────┘┴ └────┘ └─┘└─┘┴ └───┘┴ └┘┴└────
doc └───────────┘└────────┘┴ └────┘ └─┘ ┴ └───┘┴ └┘ └────
txt └───────────┘ ┴ └────┘ └─┘ ┴ ┴ └┘ └────
par └───────────┘ ┴ └────┘ └─┘ ┴ ┴ └┘ └────
pid └─┘└─┘ ┴ └────┘ └─┘ ┴ ┴ └┘ ┴└───
st ──────────────────────────────────────────────────────────
603 let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
id ┴ └┘ └────────────────────────┘ └────────────────────────┘
src ───┘ ┴ └─┘ └───┘ └──┘└────────────────────────┘└─┘ └────────────────────────┘┴ ┴
typ ───┘ ┴ └─┘┴└───┘└┘└──┘└────────────────────────┘└─┘ └────────────────────────┘┴ ┴
doc ───┘ ┴ └─┘ └───┘ └──┘ └─┘ └────────────────────────┘┴ ┴
txt ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
par ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
pid ───┘ ┴ └─┘ └───┘ └──┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
604 refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
id └────────────────────┘ └┘ ┴ └──┘
src └─────┘ └────────────────────┘└─┘ ┴ ┴ └────┘ └────────────┘
typ └─────┘ └────────────────────┘└─┘└┘┴┴┴└──┘└────┘ └────────────┘
doc └─────┘ └────────────────────┘└─┘ ┴ ┴ └────┘ └────────────┘
txt └─────┘ └─┘ ┴ ┴ └────┘ └────────────┘
par └─────┘ └─┘ ┴ ┴ └────┘ └────────────┘
pid ┴ └─┘ ┴ ┴ └────┘ └────────────┘
st ─────────────────────────────────────────────────────────────────┘└─
605 have hsum := hN n hn,
id └┘ ┴ └┘
src └───────────┘ ┴ ┴
typ └───────────┘└┘┴┴┴└┘
doc └───────────┘ ┴ ┴
txt └───────────┘ ┴ ┴
par └───────────┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴
st ─────────────────────┘└─
606 rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum,
id └──────────┘ └────────────┘ └┘
src └──┘└──────────┘└──┘└────────────┘└─┘ └───────┘
typ └──┘└──────────┘└──┘└────────────┘└─┘└┘└───────┘
doc └──┘ └──┘ └─┘ └───────┘
txt └──┘ └──┘ └─┘ └───────┘
par └──┘ └──┘ └─┘ └───────┘
pid └┘ └──┘ └─┘ ┴└──────┘
st ─────────────────┘└─────────────────────┘┴└──────┘└─
607 calc dist (f n) (f N) = dist (f N) (f n) : dist_comm _ _
id └──┘ └──┘ ┴ ┴ ┴ └───────┘
src └──┘ └──┘ └───────┘
typ └──┘ └──┘ ┴ ┴ ┴ └───────┘
doc └──┘
st ───────────────────────────────────────────────────────────
608 ... ≤ (Ico N n).sum d : dist_le_Ico_sum_of_dist_le hn (λ k _ _, hf k)
id └─┘ ┴ └────────────────────────┘ └┘ ┴ ┴ ┴ └┘
src └─┘ └────────────────────────┘
typ └─┘ ┴ └────────────────────────┘ └┘ ┴ ┴ ┴ └┘
doc └─┘ └────────────────────────┘
st ────────────────────────────────────────────────────────────────────────
609 ... ≤ abs ((Ico N n).sum d) : le_abs_self _
id └─┘ └─┘ └─────────┘
src └─┘ └─┘ └─────────┘
typ └─┘ └─┘ └─────────┘
st ──────────────────────────────────────────────
610 ... < ε : hsum
id ┴ └──┘
typ ┴ └──┘
st ───────────────┘└
611 end
st ──┘
612
613 lemma cauchy_seq_of_summable_dist [metric_space α] {f : ℕ → α}
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
614 (h : summable (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
id └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ └────────┘ ┴
src └──────┘ └──┘ └───┘ └────────┘
typ └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ └────────┘ ┴
doc └──────┘ └────────┘
615 cauchy_seq_of_dist_le_of_summable _ (λ _, le_refl _) h
id └───────────────────────────────┘ ┴ └─────┘ ┴
src └───────────────────────────────┘ └─────┘
typ └───────────────────────────────┘ ┴ └─────┘ ┴
doc └───────────────────────────────┘
616
617 lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
618 (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a))
id ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
src └──┘ └───┘ ┴ └──────┘ └─────┘ └────┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
doc └──────┘ └─────┘ └────┘ ┴
619 (n : ℕ) :
id ┴
src ┴
typ ┴
620 dist (f n) a ≤ ∑ m, d (n + m) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
621 begin
st └─────
622 refine le_of_tendsto at_top_ne_bot (tendsto_dist tendsto_const_nhds ha)
id └───────────┘ └───────────┘ └──────────┘ └────────────────┘ └┘
src └─────┘└───────────┘┴└───────────┘┴ └──────────┘┴└────────────────┘┴ └─
typ └─────┘└───────────┘┴└───────────┘┴ └──────────┘┴└────────────────┘┴└┘└─
doc └─────┘ ┴ ┴ ┴ ┴ └─
txt └─────┘ ┴ ┴ ┴ ┴ └─
par └─────┘ ┴ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────
623 (mem_at_top_sets.2 ⟨n, λ m hnm, _⟩),
id └─────────────┘ ┴
src ───┘ └─────────────┘└─┘ └┘ └─────────┘
typ ───┘ └─────────────┘└─┘ ┴└┘ └─────────┘
doc ───┘ └─┘ └┘ └─────────┘
txt ───┘ └─┘ └┘ └─────────┘
par ───┘ └─┘ └┘ └─────────┘
pid ───┘ └─┘ └┘ └─────────┘
st ──────────────────────────────────────┘└─
624 refine le_trans (dist_le_Ico_sum_of_dist_le hnm (λ k _ _, hf k)) _,
id └──────┘ └────────────────────────┘ └─┘ └┘
src └─────┘└──────┘┴ └────────────────────────┘┴ ┴ └──────┘ ┴ └──┘
typ └─────┘└──────┘┴ └────────────────────────┘┴└─┘┴ └──────┘└┘┴ └──┘
doc └─────┘ ┴ └────────────────────────┘┴ ┴ └──────┘ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └──────┘ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └──────┘ ┴ └──┘
pid ┴ ┴ ┴ ┴ └──────┘ ┴ └──┘
st ───────────────────────────────────────────────────────────────────┘└─
625 rw [sum_Ico_eq_sum_range],
id └──────────────────┘
src └──┘└──────────────────┘┴
typ └──┘└──────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────────┘└──
626 refine sum_le_tsum (range _) (λ _ _, le_trans dist_nonneg (hf _)) _,
id └─────────┘ └───┘ └──────┘ └─────────┘ └┘
src └─────┘└─────────┘┴ └───┘└──┘ └────┘└──────┘┴└─────────┘┴ └────┘
typ └─────┘└─────────┘┴ └───┘└──┘ └────┘└──────┘┴└─────────┘┴ └┘└────┘
doc └─────┘ ┴ └───┘└──┘ └────┘ ┴ ┴ └────┘
txt └─────┘ ┴ └──┘ └────┘ ┴ ┴ └────┘
par └─────┘ ┴ └──┘ └────┘ ┴ ┴ └────┘
pid ┴ ┴ └──┘ └────┘ ┴ ┴ └────┘
st ────────────────────────────────────────────────────────────────────┘└─
627 exact summable_comp_of_summable_of_injective _ hd (add_left_injective n)
id └────────────────────────────────────┘ └┘ └────────────────┘ ┴
src └────┘└────────────────────────────────────┘└─┘ ┴ └────────────────┘┴ └┘
typ └────┘└────────────────────────────────────┘└─┘└┘┴ └────────────────┘┴┴└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────┘
628 end
st └─┘
629
630 lemma dist_le_tsum_of_dist_le_of_tendsto₀ [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
631 (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) :
id ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
src └──┘ └───┘ ┴ └──────┘ └─────┘ └────┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
doc └──────┘ └─────┘ └────┘ ┴
632 dist (f 0) a ≤ tsum d :=
id └──┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘
633 by simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0
id └──────┘ └────────────────────────────────┘ ┴ └┘ └┘ └┘
src └──────────┘└──────┘└──────┘└────────────────────────────────┘┴ ┴ ┴ ┴ └──
typ └──────────┘└──────┘└──────┘└────────────────────────────────┘┴┴┴└┘┴└┘┴└┘└──
doc └──────────┘ └──────┘ ┴ ┴ ┴ ┴ └──
txt └──────────┘ └──────┘ ┴ ┴ ┴ ┴ └──
par └──────────┘ └──────┘ ┴ ┴ ┴ ┴ └──
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴└─
st └────────────────────────────────────────────────────────────────────────────
634
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
635 lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α}
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
636 (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) :
id └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └────┘ ┴ ┴
src └──────┘ └──┘ └───┘ └─────┘ └────┘ ┴
typ └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └────┘ ┴ ┴
doc └──────┘ └─────┘ └────┘ ┴
637 dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └──┘ ┴ ┴┴┴ ┴ ┴┴┴ └──┘
src └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └──┘ ┴ ┴┴┴ ┴ ┴┴┴ └──┘
doc ┴ ┴
638 show dist (f n) a ≤ ∑ m, (λx, dist (f x) (f x.succ)) (n + m), from
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘ └───┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
doc ┴ ┴
639 dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n
id └────────────────────────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └┘ ┴
src └────────────────────────────────┘ └──┘ └───┘ └─────┘
typ └────────────────────────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └┘ ┴
640
641 lemma dist_le_tsum_dist_of_tendsto₀ [metric_space α] {f : ℕ → α}
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
642 (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) :
id └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └────┘ ┴ ┴
src └──────┘ └──┘ └───┘ └─────┘ └────┘ ┴
typ └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────┘ ┴ └────┘ ┴ ┴
doc └──────┘ └─────┘ └────┘ ┴
643 dist (f 0) a ≤ ∑ n, dist (f n) (f n.succ) :=
id └──┘ ┴ ┴ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴└───┘
src └──┘ ┴ ┴ ┴ └──┘ └───┘
typ └──┘ ┴ ┴ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴└───┘
doc ┴ ┴
644 by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
id └──────┘ └──────────────────────────┘ ┴ └┘
src └──────────┘└──────┘└──────┘└──────────────────────────┘┴ ┴ └──
typ └──────────┘└──────┘└──────┘└──────────────────────────┘┴┴┴└┘└──
doc └──────────┘ └──────┘ ┴ ┴ └──
txt └──────────┘ └──────┘ ┴ ┴ └──
par └──────────┘ └──────┘ ┴ ┴ └──
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ ┴└─
st └────────────────────────────────────────────────────────────────
645
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
646 end cauchy_seq